1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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
|
GitWeb
