Imported Upstream version 8.0pl3upstream/8.0pl3

2 files changed, 37 insertions, 39 deletions

diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index b358ff39..1500e1ae 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -157,11 +157,9 @@ let rec npatternify ltypes c =
   | [] -> c
   | (mv,nme,t)::ltypes' -> 
      let c'= substitterm 0 mv (mkRel 1) c in
-(*      let _ = prconstr c' in *)
      let tlift = lift (List.length ltypes') t in
      let res = 
       npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in
-(*      let _ = prconstr res in *)
      res
 
 (* fait une application (c m1 m2...mn, où mi est une evar, on rend également
@@ -510,15 +508,15 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs:
   | u -> 
      let varrels = List.rev (List.map fst lst_vars) in
      let varnames = List.map snd lst_vars in
-     let nb_vars = (List.length varnames) in
-     let nb_eqs = (List.length lst_eqs) in
+     let nb_vars = List.length varnames in
+     let nb_eqs = List.length lst_eqs in
      let eqrels = List.map fst lst_eqs in
      (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs
         trouvés dans les let in et les Cases avec ceux trouves dans u (ie
         mi.mimick). *)
      (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *)
-     let terms_recs = lst_recs @ (hdMatchSub_cpl mi.mimick mi.fonc)  in
-     
+     let terms_recs = lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in
+
      (*c construction du terme: application successive des variables, des
        egalites et des appels rec, a la variable existentielle correspondant a
        l'hypothese de recurrence en cours. *)
@@ -573,7 +571,6 @@ let invfun_proof fonc def_fonc gl_abstr pis env sigma =
  sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false} in
  let princ_proof,levar,lposeq,evararr,absc,parms = proofPrinc mi [] [] [] in
  princ_proof,levar,lposeq,evararr,absc,parms
-
 (* Do intros [i] times, then do rewrite on all introduced hyps which are called
    like [heq_prefix], FIX: have another filter than the name. *)
 let rec iterintro i = 
@@ -596,12 +593,12 @@ let rec iterintro i =
 
 (* 
        (fun hyp gl -> 
-        let _ = print_string ("nthhyp= "^ string_of_int i) in
+        let _ = prstr ("nthhyp= "^ string_of_int i) in
         if isConst hyp && ((name_of_const hyp)==heq_prefix) then
-          let _ = print_string "YES\n" in
+          let _ = prstr "YES\n" in
           rewriteLR hyp gl 
         else 
-          let _ = print_string "NO\n" in
+          let _ = prstr "NO\n" in
           tclIDTAC gl)
  *)
     
@@ -818,9 +815,9 @@ let buildFunscheme fonc mutflist =
     
 (* Declaration of the functional scheme. *)
 let declareFunScheme f fname mutflist =
- let scheme = 
-   buildFunscheme (constr_of f) 
-    (Array.of_list (List.map constr_of (f::mutflist))) in
+ let flist = if mutflist=[] then [f] else mutflist in
+ let fcstrlist = Array.of_list (List.map constr_of flist) in
+ let scheme = buildFunscheme (constr_of f) fcstrlist in
   let _ = prstr "Principe:" in
   let _ = prconstr scheme in
  let ce = { 
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 6e086d95..a125b9a7 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -21,7 +21,7 @@ open Reductionops
 (*s printing of constr -- debugging *)
 
 (* comment this line to see debug msgs *)
-let msg x = () ;; let prterm c = str "" 
+let msg x = () ;; let prterm c = str ""
   (* uncomment this to see debugging *)
 let prconstr c =  msg (str"  " ++ prterm c ++ str"\n")
 let prlistconstr lc = List.iter prconstr lc
@@ -194,52 +194,53 @@ let rec buildrefl_from_eqs eqs =
 
 
 
-(* list of occurrences of a term inside another, no imbricated
-   occurrence are considered (ie we stop looking inside a termthat is
-   an occurrence). *)
+(* list of occurrences of a term inside another *)
+(* Cofix will be wrong, not sure Fix is correct too *)
 let rec hdMatchSub u t=
-  if constr_head_match u t then 
-	 u::(fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
-      [] 
-      u)
-  else
-    fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
-      [] 
-      u
+  let subres = 
+    match kind_of_term u with
+      | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t
+      | Fix (_,(lna,tl,bl))  -> 
+	  Array.fold_left 
+	    (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t) 
+	    [] bl
+      | LetIn _  -> assert false
+	  (* Correct? *)
+      | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u
+  in 
+  if constr_head_match u t then u :: subres else subres
+
 
 (* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *)
 let hdMatchSub_cpl u (d,f) = 
-	 let res = ref [] in
-	 begin
-	 	for i = d to f do res := (hdMatchSub u (mkRel i)) @ !res done;
-		  !res
-	 end
+  let res = ref [] in
+  begin
+    for i = d to f do res := hdMatchSub u (mkRel i) @ !res done;
+    !res
+  end
 
 
 (* destApplication raises an exception if [t] is not an application *)      
 let exchange_hd_prod subst_hd t =
-    let (hd,args)= destApplication t in mkApp (subst_hd,args)
+  let hd,args= destApplication t in mkApp (subst_hd,args)
 
 (* substitute t by by_t in head of products inside in_u, reduces each
 	product found  *)
 let rec substit_red prof t by_t in_u =
   if constr_head_match in_u (lift prof t) 
   then
-	 let _ = prNamedConstr "in_u" in_u in
-	 let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
-	 let _ = prNamedConstr "xx " x in
-	 let _ = prstr "\n\n" in
-	 x
+    let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
+    x
   else
-    map_constr_with_binders succ (fun i u -> substit_red i t by_t u)
-    	prof in_u
+    map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u
 
 (* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each
 	reli by tarr.(f-i). *) 
 let exchange_reli_arrayi tarr (d,f) t =
   let hd,args= destApplication t in 
   let i = destRel hd in
-  whd_beta (mkApp (tarr.(f-i) ,args))
+  let res = whd_beta (mkApp (tarr.(f-i) ,args)) in
+  res
 
 let exchange_reli_arrayi_L tarr (d,f) = 
   List.map (exchange_reli_arrayi tarr (d,f))