Coq 8.0pl1 et ocaml 3.08.1
Bonjour,
[ English summary: here is a patch fixing Coq 8.0pl1 for it to compile
under OCaml 3.08.1. ]
On ne peut pas recompiler Coq 8.0 avec OCaml 3.08.1 à cause d'un bug
Camlp4 que j'ai réparé dans cette dernière version.
Les erreurs sont limitées à contrib/funind/tacinv.ml4 qui utilise des
expressions OCaml du style
fun x,y,z -> e
voire même
fun acc x,y -> e
qui sont illégales en OCaml mais ont été acceptées par erreur par
Camlp4 jusqu'à 3.08.0 incluse.
Vous trouverez ci-joint un patch qui permet la compilation de Coq.
J'aurai appris dans cette affaire que réparer des bugs dans une
"bugfix release" n'est pas toujours une bonne idée (disons qu'il faut
recompiler Coq avant de commit-ter les bugfixes).
Désolé pour ces ennuis. Amicalement,
-- Michel
--- 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
Reply to: