diff options
author | Olivier Fisette <ribosome@gentoo.org> | 2004-12-28 05:03:02 +0000 |
---|---|---|
committer | Olivier Fisette <ribosome@gentoo.org> | 2004-12-28 05:03:02 +0000 |
commit | b7a8f1da5f05d8b67a43f5a5238609eaa436292a (patch) | |
tree | 16f253fb84d6e517a7ca7d6d9a033be156091818 /sci-mathematics/coq/files | |
parent | Moving to sci-mathematics/coq (diff) | |
download | gentoo-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.patch | 20 | ||||
-rw-r--r-- | sci-mathematics/coq/files/coq-8.0-ocaml-3.08.1.patch | 29 | ||||
-rw-r--r-- | sci-mathematics/coq/files/coqide.desktop | 10 | ||||
-rw-r--r-- | sci-mathematics/coq/files/digest-coq-7.4 | 1 | ||||
-rw-r--r-- | sci-mathematics/coq/files/digest-coq-8.0 | 2 | ||||
-rw-r--r-- | sci-mathematics/coq/files/digest-coq-8.0-r1 | 2 | ||||
-rw-r--r-- | sci-mathematics/coq/files/ocaml-3.07.patch | 10 |
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 + |