summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorOlivier Fisette <ribosome@gentoo.org>2004-12-28 05:03:02 +0000
committerOlivier Fisette <ribosome@gentoo.org>2004-12-28 05:03:02 +0000
commitb7a8f1da5f05d8b67a43f5a5238609eaa436292a (patch)
tree16f253fb84d6e517a7ca7d6d9a033be156091818 /sci-mathematics/coq/files
parentMoving to sci-mathematics/coq (diff)
downloadgentoo-2-b7a8f1da5f05d8b67a43f5a5238609eaa436292a.tar.gz
gentoo-2-b7a8f1da5f05d8b67a43f5a5238609eaa436292a.tar.bz2
gentoo-2-b7a8f1da5f05d8b67a43f5a5238609eaa436292a.zip
Moved from app-sci/coq to sci-mathematics/coq.
Diffstat (limited to 'sci-mathematics/coq/files')
-rw-r--r--sci-mathematics/coq/files/coq-8.0-byteflags.patch20
-rw-r--r--sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch29
-rw-r--r--sci-mathematics/coq/files/coqide.desktop10
-rw-r--r--sci-mathematics/coq/files/digest-coq-7.41
-rw-r--r--sci-mathematics/coq/files/digest-coq-8.02
-rw-r--r--sci-mathematics/coq/files/digest-coq-8.0-r12
-rw-r--r--sci-mathematics/coq/files/ocaml-3.07.patch10
7 files changed, 74 insertions, 0 deletions
diff --git a/sci-mathematics/coq/files/coq-8.0-byteflags.patch b/sci-mathematics/coq/files/coq-8.0-byteflags.patch
new file mode 100644
index 000000000000..7b4acf017689
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.0-byteflags.patch
@@ -0,0 +1,20 @@
+--- Makefile.orig 2004-06-19 23:53:43.231742696 +0200
++++ Makefile 2004-06-19 23:54:39.977116088 +0200
+@@ -346,7 +346,7 @@
+
+ $(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO)
+ $(SHOW)'COQMKTOP -o $@'
+- $(HIDE)$(COQMKTOP) -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
++ $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@
+
+ $(COQTOP):
+ cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
+@@ -570,7 +570,7 @@
+
+ $(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) ide/ide.cma
+ $(SHOW)'COQMKTOP -o $@'
+- $(HIDE)$(COQMKTOP) -g -ide -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
++ $(HIDE)$(COQMKTOP) -g -ide -top $(BYTEFLAGS) -o $@
+
+ $(COQIDE):
+ cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
diff --git a/sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch b/sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch
new file mode 100644
index 000000000000..39f57e16521e
--- /dev/null
+++ b/sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch
@@ -0,0 +1,29 @@
+--- contrib/funind/tacinv.ml4.orig 2004-02-10 17:22:14.000000000 +0100
++++ contrib/funind/tacinv.ml4 2004-08-20 13:29:59.000000000 +0200
+@@ -495,7 +495,7 @@
+ let metav = mknewmeta() in
+ let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in
+ let newrec_call = substmeta rec_call in
+- let newlevar = List.map (fun ev,tev -> ev, substmeta tev) levar in
++ let newlevar = List.map (fun (ev,tev) -> ev, substmeta tev) levar in
+ let newabsc = Array.map substmeta absc in
+ newrec_call,newlevar,lposeq,evararr,newabsc,((metav,nme, typ)::parms)
+
+@@ -693,7 +693,7 @@
+ (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
+ let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in
+ (* apply parameters immediately *)
+- let gl_abstr = applistc gl_abstr' (List.map (fun x,y,z -> x) (List.rev parms)) in
++ let gl_abstr = applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev parms)) in
+
+ (* we apply args of the fix now, the parameters will be applied later *)
+ let princ_proof_applied_args =
+@@ -790,7 +790,7 @@
+ in
+ let rec princ_replace_params params t =
+ List.fold_left (
+- fun acc ev,nam,typ ->
++ fun acc (ev,nam,typ) ->
+ mkLambda (Name (id_of_name nam) , typ,
+ substitterm 0 ev (mkRel 1) (lift 0 acc)))
+ t (List.rev params) in
diff --git a/sci-mathematics/coq/files/coqide.desktop b/sci-mathematics/coq/files/coqide.desktop
new file mode 100644
index 000000000000..08b5b6918cd0
--- /dev/null
+++ b/sci-mathematics/coq/files/coqide.desktop
@@ -0,0 +1,10 @@
+[Desktop Entry]
+Encoding=UTF-8
+Comment=Coq integrated developpment environment
+Icon=/usr/lib/coq/ide/coq.png
+Exec=/usr/bin/coqide
+Name=CoqIDE
+GenericName=Coq IDE
+Terminal=false
+Type=Application
+Categories=Application;Edutainment;Mathematics;
diff --git a/sci-mathematics/coq/files/digest-coq-7.4 b/sci-mathematics/coq/files/digest-coq-7.4
new file mode 100644
index 000000000000..ab1d3353a4d9
--- /dev/null
+++ b/sci-mathematics/coq/files/digest-coq-7.4
@@ -0,0 +1 @@
+MD5 13ac61f150823e54ad84a9096e2dd646 coq-7.4.tar.gz 1537547
diff --git a/sci-mathematics/coq/files/digest-coq-8.0 b/sci-mathematics/coq/files/digest-coq-8.0
new file mode 100644
index 000000000000..c339254dca9e
--- /dev/null
+++ b/sci-mathematics/coq/files/digest-coq-8.0
@@ -0,0 +1,2 @@
+MD5 75ab1eb131b3469d21ab74377826b32b coq-8.0.tar.gz 2281827
+MD5 e2e4ecc8a552c847a656dcf9e47dd738 coq-8.0-translator.tar.gz 233218
diff --git a/sci-mathematics/coq/files/digest-coq-8.0-r1 b/sci-mathematics/coq/files/digest-coq-8.0-r1
new file mode 100644
index 000000000000..73335eb85772
--- /dev/null
+++ b/sci-mathematics/coq/files/digest-coq-8.0-r1
@@ -0,0 +1,2 @@
+MD5 95237e64081d7306fdea49e1988bde12 coq-8.0pl1.tar.gz 2272613
+MD5 58a3c3c6e3903b0267857d283047c7e3 coq-8.0pl1-translator.tar.gz 233233
diff --git a/sci-mathematics/coq/files/ocaml-3.07.patch b/sci-mathematics/coq/files/ocaml-3.07.patch
new file mode 100644
index 000000000000..707c51039b8a
--- /dev/null
+++ b/sci-mathematics/coq/files/ocaml-3.07.patch
@@ -0,0 +1,10 @@
+--- /root/tmp/coq-7.4/parsing/pcoq.ml4 2002-12-15 13:10:18.000000000 +0100
++++ parsing/pcoq.ml4 2003-10-16 13:00:15.000000000 +0200
+@@ -108,6 +108,7 @@
+ type parsable = G.parsable
+ let parsable = G.parsable
+ let tokens = G.tokens
++ let glexer = G.glexer
+ module Entry = G.Entry
+ module Unsafe = G.Unsafe
+