Add patch for ocaml-3.08.1

diff --git a/app-sci/coq/ChangeLog b/app-sci/coq/ChangeLog
index 97dc87cb3472d98c66fc25cbd70eeefb6e2a5f1f..e751c48656b57bef31d79a36f12a82ea51988c84 100644 (file)
--- a/app-sci/coq/ChangeLog
+++ b/app-sci/coq/ChangeLog
@@ -1,6 +1,10 @@
 # ChangeLog for app-sci/coq
 # Copyright 2000-2004 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/ChangeLog,v 1.8 2004/08/14 04:42:52 weeve Exp $
+# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/ChangeLog,v 1.9 2004/11/18 22:52:52 mattam Exp $
+
+  18 Nov 2004; Matthieu Sozeau <mattam@gentoo.org>
+  +files/coq-8.0-ocaml-3.08.1.patch, coq-8.0-r1.ebuild:
+  Add patch for ocaml-3.08.1.
 
   13 Aug 2004; Jason Wever <weeve@gentoo.org> coq-8.0-r1.ebuild:
   Added ~sparc keyword.

diff --git a/app-sci/coq/Manifest b/app-sci/coq/Manifest
index c00c12dff13c03083fa4419c957f2bd6e471d6c3..0d8a82e0cdcc80ef4e51f9f77359f1b94b0d93e3 100644 (file)
--- a/app-sci/coq/Manifest
+++ b/app-sci/coq/Manifest
@@ -1,11 +1,12 @@
-MD5 1e1b2a26dc57dbb1765cbb2b553d398c ChangeLog 1399
+MD5 4b3e22466363130a7a799228534043a2 coq-8.0.ebuild 1910
 MD5 2559fb0ebf76645f855752a3a18fa7d2 coq-7.4.ebuild 975
+MD5 c919fa171c61513b8683d11944adc86b ChangeLog 1538
 MD5 5af6b26df9264817e5b6a292c1436417 metadata.xml 238
-MD5 4b3e22466363130a7a799228534043a2 coq-8.0.ebuild 1910
-MD5 10df3ee1a69584eddf40eb9ad0493471 coq-8.0-r1.ebuild 1948
+MD5 da62f53c7b4fab39a73e5f847ac5cad5 coq-8.0-r1.ebuild 2056
+MD5 02ac210c6af5d8e258a2805a22822a8b files/coq-8.0-ocaml-3.08.1.patch 1321
+MD5 dc0f737371101bc7c97b0a80165ddac6 files/digest-coq-8.0-r1 136
 MD5 d3f33f3602d82ea691f91b062dbf236b files/digest-coq-7.4 60
+MD5 86922705a72292e7508baae5bc75e2a3 files/digest-coq-8.0 130
 MD5 393c3085f82f205122b4e66c94232ff7 files/ocaml-3.07.patch 333
 MD5 5d46723c29afcd1e24e529e5993c3096 files/coq-8.0-byteflags.patch 676
 MD5 e5491c930f8f944ed9c3590fdc8492c1 files/coqide.desktop 242
-MD5 86922705a72292e7508baae5bc75e2a3 files/digest-coq-8.0 130
-MD5 dc0f737371101bc7c97b0a80165ddac6 files/digest-coq-8.0-r1 136

diff --git a/app-sci/coq/coq-8.0-r1.ebuild b/app-sci/coq/coq-8.0-r1.ebuild
index 14497994a124defe86d0088fbeb1a568cb9811b7..ae03d88c7eb54dd5035f788394deb3e1916f15f4 100644 (file)
--- a/app-sci/coq/coq-8.0-r1.ebuild
+++ b/app-sci/coq/coq-8.0-r1.ebuild
@@ -1,6 +1,6 @@
 # Copyright 1999-2004 Gentoo Foundation
 # Distributed under the terms of the GNU General Public License v2
-# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-8.0-r1.ebuild,v 1.2 2004/08/14 04:42:52 weeve Exp $
+# $Header: /var/cvsroot/gentoo-x86/app-sci/coq/coq-8.0-r1.ebuild,v 1.3 2004/11/18 22:52:52 mattam Exp $
 
 inherit eutils
 
@@ -29,6 +29,11 @@ src_unpack()
 {
        unpack ${A}
        cd ${S}
+       version=`ocamlc -v | grep 3.08.1`
+       if [ $? -eq 0 ]
+       then
+               epatch ${FILESDIR}/${P}-ocaml-3.08.1.patch
+       fi
        epatch ${FILESDIR}/${P}-byteflags.patch
 }
 

diff --git a/app-sci/coq/files/coq-8.0-ocaml-3.08.1.patch b/app-sci/coq/files/coq-8.0-ocaml-3.08.1.patch
new file mode 100644 (file)
index 0000000..39f57e1
--- /dev/null
+++ b/app-sci/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