Correcting a bug occuring when the mimicked function had a

lambda-abstraction inside a Cases. I had to make the term of the
induction principle a bit less clean (more eta expansions).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3817 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 306 insertions, 208 deletions

diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index e845f32358..6bc310460d 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -4,7 +4,8 @@
 (* Use:
    \begin{itemize}
    \item The Tacinv directory must be in the path (-I <path> option)
-   \item use the bytecode version of coqtop or coqc (-byte option), or make a coqtop
+   \item use the bytecode version of coqtop or coqc (-byte option), or make a
+         coqtop 
    \item Do [Require Tacinv] to be able to use it.
    \item For syntax see Tacinv.v
    \end{itemize}
@@ -36,13 +37,16 @@ open Vernacinterp
 open Evd
 open Environ
 open Entries
- (*i*)
+open Setoid_replace
 open Tacinvutils
+(*i*)
 
 module Smap = Map.Make(struct type t = constr let compare = compare end)
 let smap_to_list m = Smap.fold (fun c cb l -> (c,cb)::l) m []
 let merge_smap m1 m2 = Smap.fold (fun c cb m -> Smap.add c cb m) m1 m2
 
+let mkthesort = mkProp (* would like to put Type here, but with which index? *)
+
 (*  this is the prefix used to name equality hypothesis generated by
     case analysis*)
 let equality_hyp_string = "_eg_"
@@ -57,18 +61,15 @@ let debug i = prstr ("DEBUG "^ string_of_int i ^"\n")
 let pr2constr = (fun c1 c2 -> prconstr c1; prstr " <---> "; prconstr c2)
  (*end debugging *)
 
-let constr_of c = 
- try Constrintern.interp_constr Evd.empty (Global.env()) c
- with _ -> 
-  msg (str "constr_of: error when looking for term: "); 
-  raise Not_found
+let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
 
 let rec collect_cases l =
  match l with
   | [||] -> [||],[],[],[||],[||]
   | arr -> 
      let (a,c,d,f,e)= arr.(0) in
-     let aa,lc,ld,_,_ = collect_cases (Array.sub arr 1 ((Array.length arr)-1)) in
+     let aa,lc,ld,_,_ = 
+      collect_cases (Array.sub arr 1 ((Array.length arr)-1)) in
      Array.append [|a|] aa , (c@lc) , (d@ld) , f , e
 
 let rec collect_pred l =
@@ -79,16 +80,21 @@ let rec collect_pred l =
 
 (*s specific manipulations on constr *)
 let lift1_leqs leq=
- List.map (function typofg,g,d -> lift 1 typofg, lift 1 g , lift 1 d) leq
+ List.map 
+  (function (r,(typofg,g,d)) 
+      -> lift 1 r, (lift 1 typofg, lift 1 g , lift 1 d)) leq
 
-(* WARNING: In the types, we don't lift the rels in the type. This is intentional. Use
-  with care. *)
+let lift1_relleqs leq= List.map (function (r,x) -> lift 1 r,x) leq
+
+(* WARNING: In the types, we don't lift the rels in the type. This is
+   intentional. Use with care. *)
 let lift1_lvars lvars= List.map 
  (function x,(nme,c) -> lift 1 x, (nme, (*lift 1*) c)) lvars
 
+
 let rec add_n_dummy_prod t n = 
  if n<=0 then t
- else add_n_dummy_prod (mkNamedProd (id_of_string "DUMMY") mkProp t) (n-1)
+ else add_n_dummy_prod (mkNamedProd (id_of_string "DUMMY") mkthesort t) (n-1)
 
 (* [add_lambdas t gl [csr1;csr2...]] returns [[x1:type of csr1]
    [x2:type of csr2] t [csr <- x1 ...]], names of abstracted variables
@@ -112,13 +118,14 @@ let rec add_pis t gl lcsr =
 let mkProdEg teq eql eqr concl =
  mkProd (name_of_string "eg", mkEq teq eql eqr, lift 1 concl)
 
-let eqs_of_beqs = List.map (function a,b,c -> (Anonymous, mkEq a b c))
+let eqs_of_beqs x = 
+ List.map (function (_,(a,b,c)) -> (Anonymous, mkEq a b c)) x
 
 
 let rec eqs_of_beqs_named_aux s i l =
  match l with 
   | [] -> []
-  | (a,b,c)::l' -> 
+  | (r,(a,b,c))::l' -> 
      (Name(id_of_string (s^ string_of_int i)), mkEq a b c)
      ::eqs_of_beqs_named_aux s (i-1) l'
 
@@ -143,9 +150,11 @@ let rec apply_levars c lmetav =
          ((exkey,typ)::levars), mkCast ((applistc trm [mkEvar exkey]),typ) *)
 
 
-let prod_change_concl c newconcl = let lv,_ = decompose_prod c in prod_it  newconcl lv
+let prod_change_concl c newconcl = 
+ let lv,_ = decompose_prod c in prod_it  newconcl lv
 
-let lam_change_concl c newconcl = let lv,_ = decompose_prod c in lam_it newconcl lv
+let lam_change_concl c newconcl = 
+ let lv,_ = decompose_prod c in lam_it newconcl lv
 
 
 let rec mkAppRel c largs n =
@@ -171,16 +180,16 @@ let rec build_rel_map typ type_of_b =
   | App (f,args), App (fb,argsb) ->
      (try build_rel_map_list (Array.to_list args) (Array.to_list argsb)
      with Invalid_argument _ -> 
-      failwith ("Could not generate caes annotation. "^ 
-      "To application with different length"))
+      failwith ("Could not generate case annotation. "^ 
+      "Two application with different length"))
   | Const c1, Const c2 -> if c1=c2 then Smap.empty
-    else failwith ("Could not generate caes annotation. "^ 
-    "To different constants in a case annotation.")
+    else failwith ("Could not generate case annotation. "^ 
+    "Two different constants in a case annotation.")
   | Ind c1, Ind c2 -> if c1=c2 then Smap.empty
-    else failwith ("Could not generate caes annotation. "^ 
-    "To different constants in a case annotation.")
+    else failwith ("Could not generate case annotation. "^ 
+    "Two different constants in a case annotation.")
   | _,_ -> failwith ("Could not generate case annotation. "^
-    "Incompatibility between annotation and actal type")
+    "Incompatibility between annotation and actual type")
 and build_rel_map_list ltyp ltype_of_b =
  List.fold_left2 (fun a b c -> merge_smap a (build_rel_map b c))
   Smap.empty ltyp ltype_of_b
@@ -190,64 +199,92 @@ and build_rel_map_list ltyp ltype_of_b =
 
 (*
   \begin {itemize}
-  \item [concl] ([constr]): conclusions, cad (xi:ti)gl, ou gl  est le but a prouver, et
-  xi:ti correspondent aux  arguments donnés à la tactique.  On enlève un produit à
-  chaque fois qu'on rencontre un binder, sans lift ou pop.  Initialement: une
-  seule conclusion, puis specifique a  chaque branche. 
+  \item [concl] ([constr]): conclusions, cad (xi:ti)gl, ou gl est le but a
+  prouver, et xi:ti correspondent aux arguments donnés à la tactique.  On
+  enlève un produit à chaque fois qu'on rencontre un binder, sans lift ou pop.
+  Initialement: une seule conclusion, puis specifique a chaque branche.
   \item[absconcl] ([constr array]): les conclusions (un predicat pour chaque
   fixp. mutuel) patternisées pour  pouvoir être appliquées.
-  \item [mimick] ([constr]): le terme qu'on imite. On plonge  dedans au fur et à mesure,
-  sans lift ni pop. 
-  \item [nmefonc] ([constr array]): la constante correspondant à la fonction appelée,
-  permet de remplacer les appels recursifs par des appels à la constante
-  correspondante (non pertinent (et inutile) si on permet l'appel de la tactique
-  sur une terme donné directement (au lieu d'une constante comme pour l'instant)).
-  \item [fonc] ([int array]) : indices des variable correspondant aux appels récursifs
-  (plusieurs car fixp.  mutuels), utile pour reconnaître les appels récursifs
-  (ATTENTION: initialement vide, reste vide tant qu'on n'est pas dans un fix.).
-  
-  \item [lst_vars] ([(constr*(name*constr)) list]): liste des variables rencontrées
-  jusqu'à maintenant.
-  \item [lst_eqs] ([constr list]): liste d'équations engendrées au cours du parcours,
-  cette liste grandit à  chaque case, et il faut lifter le tout à chaque binder.
-  \item [lst_recs] ([constr list]): listes des appels  récursifs rencontrés jusque
-  là.
+  \item [mimick] ([constr]): le terme qu'on imite. On plonge  dedans au fur et
+  à mesure, sans lift ni pop.
+  \item [nmefonc] ([constr array]): la constante correspondant à la fonction
+  appelée, permet de remplacer les appels recursifs par des appels à la
+  constante correspondante (non pertinent (et inutile) si on permet l'appel de
+  la tactique sur une terme donné directement (au lieu d'une constante comme
+  pour l'instant)).
+  \item [fonc] ([int*int]) : bornes des indices des variable correspondant aux
+  appels récursifs (plusieurs car fixp.  mutuels), utile pour reconnaître les
+  appels récursifs (ATTENTION: initialement vide, reste vide tant qu'on n'est
+  pas dans un fix).  
+  \end{itemize}
+*)
+
+type mimickinfo =
+    {
+     concl: constr;
+     absconcl: constr array;
+     mimick: constr;
+     env: env;
+     sigma: Evd.evar_map;
+     nmefonc: constr array;
+     fonc: int * int;
+     doeqs: bool (* this reference is to toggle building of equalities during
+                    the building of the principle (default is true) *)
+    }
+
+(*
+  \begin{itemize}
+  \item [lst_vars] ([(constr*(name*constr)) list]): liste des variables
+  rencontrées jusqu'à maintenant.
+  \item [lst_eqs] ([constr list]): liste d'équations engendrées au cours du
+  parcours, cette liste grandit à chaque case, et il faut lifter le tout à
+  chaque binder.
+  \item [lst_recs] ([constr list]): listes des appels récursifs rencontrés
+  jusque là.
   \end{itemize}
-  
-  le Compteur nthhyp est utilisé pour contourner un comportement bizarre de refine en
-  beta expansant lesmutual fixpt. On mets une variable à la place d'un ?, dont le
-  debruijn pointe sur la nieme hypothèse (nthhyp). nthhyp vaut donc initialement 1.
 
   Cette fonction rends un nuplet de la forme:
 
-  [t,[(ev1,tev1);(ev2,tev2)..],[(i1,j1,k1);(i2,j2,k2)..],[|c1;c2..|],[|typ1;typ2..|]]
+  [t,
+  [(ev1,tev1);(ev2,tev2)..],
+  [(i1,j1,k1);(i2,j2,k2)..],
+  [|c1;c2..|],
+  [|typ1;typ2..|]]
 
   où:
-  \begin{itemize}
-  \item[t] est le principe demandé, il contient des meta variables représentant soit des
-  trous à prouver plus tard, soit les conclusions à compléter avant de rendre le terme
-  (plusieurs conclusions si plusieurs fonction mutuellement récursives) voir la suite.
-  \item[[(ev1,tev1);(ev2,tev2)...]] est l'ensemble des méta variables correspondant à
-  des trous. [evi] est la meta variable, [tevi] est son type.
-  \item[(in,jn,kn)] sont les nombres respectivement de variables, d'équations, et
-  d'hypothèses de récurrence pour le but n. Permet de faire le bon nombre d'intros et
-  des rewrite au bons endroits dans la suite.
-  \item[[|c1;c2...|]] est un tableau de meta variables correspondant à chacun des
-  prédicats mutuellement récursifs construits.
-  \item[|typ1;typ2...|] est un tableau contenant les conclusions respectives de chacun
-  des prédicats mutuellement récursifs. Permet de finir la construction du principe.
+
+  \begin{itemize} 
+
+  \item[t] est le principe demandé, il contient des meta variables représentant
+  soit des trous à prouver plus tard, soit les conclusions à compléter avant de
+  rendre le terme (plusieurs conclusions si plusieurs fonction mutuellement
+  récursives) voir la suite.
+
+  \item[[(ev1,tev1);(ev2,tev2)...]] est l'ensemble des méta variables
+  correspondant à des trous. [evi] est la meta variable, [tevi] est son type.
+
+  \item[(in,jn,kn)] sont les nombres respectivement de variables, d'équations,
+  et d'hypothèses de récurrence pour le but n. Permet de faire le bon nombre
+  d'intros et des rewrite au bons endroits dans la suite.
+
+  \item[[|c1;c2...|]] est un tableau de meta variables correspondant à chacun
+  des prédicats mutuellement récursifs construits.
+
+  \item[|typ1;typ2...|] est un tableau contenant les conclusions respectives de
+  chacun des prédicats mutuellement récursifs. Permet de finir la construction
+  du principe.
+
   \end{itemize}
+*)
 
-  TODO: mettre tout ça dans un record bien propre.
+type kind_of_hyp = Var | Eq  (*| Rec*)
 
-  proofPrinc G=concl absG=absconcl t=mimick X=fonc Gamma1=lst_vars Gamma2=lst_eq
-  Gamma3=lst_recs *) 
-let rec 
- proofPrinc ~concl ~absconcl ~mimick ~env ~sigma nmefonc fonc lst_vars lst_eqs lst_recs
- : constr* (constr*Term.types) list * (int*int*int) list * constr array * types array =
- match kind_of_term mimick with
-    (* Fixpoint: we reproduce the Fix, fonc becomes (1,nbofmutf) to
-      	point on the name of recursive calls *)
+let rec proofPrinc (mi:mimickinfo) lst_vars lst_eqs lst_recs:
+ constr * (constr*Term.types) list * (int*int*int) list 
+ * constr array * types array =
+ match kind_of_term mi.mimick with
+    (* Fixpoint: we reproduce the Fix, fonc becomes (1,nbofmutf) to point on
+       the name of recursive calls *) 
   | Fix((iarr,i),(narr,tarr,carr)) -> 
 
      (* We construct the right predicates for each mutual fixpt *)     
@@ -266,7 +303,7 @@ let rec
      let evararr = Array.of_list evarl in
      let pisarr = Array.of_list pisl in
      
-     let newenv = push_rec_types (narr,tarr,carr) env in
+     let newenv = push_rec_types (narr,tarr,carr) mi.env in
 
      let rec collect_fix n =
       if n >= Array.length iarr then [],[],[],[]
@@ -275,17 +312,18 @@ let rec
         let c = Array.get carr n in
         (* rappelle sur le sous-terme, on ajoute un niveau de
            profondeur (lift) parce que Fix est un binder. *)
-        let appel_rec,levar,lposeq,_,evarrarr =
-         proofPrinc ~concl:(pisarr.(n)) ~absconcl:newabsconcl ~mimick:c nmefonc
-         (1,((Array.length iarr))) ~env:newenv ~sigma:sigma (lift1_lvars lst_vars)
-         (lift1_leqs lst_eqs) (lift1L lst_recs) in
+        let newmi = {mi with concl=(pisarr.(n)); absconcl=newabsconcl;
+        mimick=c; fonc=(1,((Array.length iarr)));env=newenv} in
+        let appel_rec,levar,lposeq,_,evarrarr = 
+         proofPrinc newmi (lift1_lvars lst_vars) 
+          (lift1_leqs lst_eqs) (lift1L lst_recs) in
         let lnme,lappel_rec,llevar,llposeq = collect_fix (n+1) in
         (nme::lnme),(appel_rec::lappel_rec),(levar@llevar), (lposeq@llposeq) in
      let lnme,lappel_rec,llevar,llposeq =collect_fix  0 in
      let lnme' = List.map (fun nme -> newname_append nme   "_ind") lnme in
      let anme = Array.of_list lnme' in
      let aappel_rec = Array.of_list lappel_rec in
-     mkFix((iarr,i), ( anme, pisarr ,aappel_rec)), llevar,llposeq,evararr,pisarr
+     mkFix((iarr,i),(anme, pisarr,aappel_rec)),llevar,llposeq,evararr,pisarr
 
   (* <pcase> Cases b of arrPt end.*)
   | Case(cinfo, pcase, b, arrPt) -> 
@@ -293,33 +331,50 @@ let rec
      let prod_pcase,_ = decompose_lam pcase in
      let nmeb,lastprod_pcase = List.hd prod_pcase in
      let b'= apply_leqtrpl_t b lst_eqs in
-     let type_of_b = Typing.type_of env sigma b in
-     let new_lst_recs = lst_recs @ hdMatchSub_cpl b fonc in
+     let type_of_b = Typing.type_of mi.env mi.sigma b in
+     let new_lst_recs = lst_recs @ hdMatchSub_cpl b mi.fonc in
      (* Replace the calls to the function (recursive calls) by calls to the
         corresponding constant:  *)
-     let d,f = fonc in 
+     let d,f = mi.fonc in 
      let res = ref b' in
      let _ = for i = d to f do 
-       res := substitterm 0 (mkRel i) nmefonc.(f-i) !res done in
+       res := substitterm 0 (mkRel i) mi.nmefonc.(f-i) !res done in
      let newb = !res in
 
-     (* [fold_proof t l n] rend le resultat de l'appel recursif sur les elements de la
-        liste l (correpsondant a arrPt), appele avec les bons arguments: [concl] devient
-        [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n] est le nombre d'arguments du
-        constructeur considéré (FIX: Hormis les parametres!!), et [concl'] est concl ou
-        l'on a réécrit [b] en ($c_n$ [rel1]...).*)
+     (* [fold_proof t l n] rend le resultat de l'appel recursif sur les
+        elements de la liste l (correpsondant a arrPt), appele avec les bons
+        arguments: [concl] devient [(DUMMY1:t1;...;DUMMY:tn)concl'], ou [n]
+        est le nombre d'arguments du constructeur considéré (FIX: Hormis les
+        parametres!!), et [concl'] est concl ou l'on a réécrit [b] en ($c_n$
+        [rel1]...).*)
 
      let rec fold_proof nth_construct eltPt' =  
       (* mise a jour de concl pour l'interieur du case, concl'= concl[b <- C x3
          x2 x1... ], sans quoi les annotations ne sont plus coherentes *)
       let cstr_appl,nargs = nth_dep_constructor type_of_b nth_construct in
-      let concl'' = substitterm 0 (lift nargs b) cstr_appl (lift nargs concl) in
+      let concl'' = 
+       substitterm 0 (lift nargs b) cstr_appl (lift nargs mi.concl) in
+      let neweq = mkEq type_of_b newb (popn nargs cstr_appl) in
       let concl_dummy = add_n_dummy_prod concl'' nargs in
-      let lsteqs_rew =
-       apply_eq_leqtrpl lst_eqs (mkEq type_of_b newb (popn nargs cstr_appl)) in
-      let new_lsteqs = (type_of_b,newb, popn nargs cstr_appl)::lsteqs_rew in
-      proofPrinc ~concl:concl_dummy ~absconcl:absconcl ~mimick:eltPt' ~env:env
-       ~sigma:sigma nmefonc fonc lst_vars new_lsteqs new_lst_recs in
+      let lsteqs_rew = apply_eq_leqtrpl lst_eqs neweq in
+      let new_lsteqs = 
+       (mkRel (0-nargs),(type_of_b,newb, popn nargs cstr_appl))::lsteqs_rew in
+      let a',a'' = decompose_lam_n nargs eltPt' in
+      let newa'' = 
+       if mi.doeqs 
+       then mkLambda (name_of_string "_eq_",lift nargs neweq,lift 1 a'') 
+       else a'' in
+      let newmimick = lamn nargs a' newa'' in
+      let b',b'' = decompose_prod_n nargs concl_dummy in
+      let newb'' = 
+       if mi.doeqs 
+       then mkProd (name_of_string "_eq_",lift nargs neweq,lift 1 b'')
+       else b'' in
+      let newconcl = prodn nargs b' newb'' in
+      let newmi = {mi with mimick=newmimick; concl=newconcl} in
+      let a,b,c,d,e = proofPrinc newmi lst_vars new_lsteqs new_lst_recs in
+      a,b,c,d,e
+      in
      
      let arrPt_proof,levar,lposeq,evararr,absc = 
       collect_cases (Array.mapi fold_proof arrPt) in
@@ -329,18 +384,21 @@ let rec
      (* je remplace b par rel1 (apres avoir lifte un coup) dans la
         future annotation du futur case: ensuite je mettrai un lambda devant *)
      let typesofeqs' = eqs_of_beqs_named equality_hyp_string lst_eqs in
-     let typesofeqs = prod_it_lift  typesofeqs' concl in
-     let typeof_case'' = substitterm 0 (lift 1 b) (mkRel 1) (lift 1 typesofeqs) in
+     (*      let typesofeqs = prod_it_lift typesofeqs' mi.concl in *)
+     let typesofeqs = mi.concl in
+     let typeof_case'' = 
+      substitterm 0 (lift 1 b) (mkRel 1) (lift 1 typesofeqs) in
      
-     (* C'est un peu compliqué ici: en cas de type inductif vraiment dépendant le
-        piquant du case [pcase] contient des lambdas supplémentaires en tête je les
-        ai dans la variable [suppllam_pcase]. Le problème est que la conclusion du
-        piquant doit faire référence à ces variables plutôt qu'à celle de
-        l'exterieur. Ce qui suit permet de changer les reference de newpacse' pour
-        pointer vers les lambda du piquant. On procède comme suit: on repère les rels
-        qui pointent à l'interieur du piquant dans la fonction imitée, pour ça on
-        parcourt le dernier lambda du piquant (qui contient le type de l'argument du
-        case), et on remplace les rels correspondant dans la preuve construite. *)
+     (* C'est un peu compliqué ici: en cas de type inductif vraiment dépendant
+        le piquant du case [pcase] contient des lambdas supplémentaires en tête
+        je les ai dans la variable [suppllam_pcase]. Le problème est que la
+        conclusion du piquant doit faire référence à ces variables plutôt qu'à
+        celle de l'exterieur. Ce qui suit permet de changer les reference de
+        newpacse' pour pointer vers les lambda du piquant. On procède comme
+        suit: on repère les rels qui pointent à l'interieur du piquant dans la
+        fonction imitée, pour ça on parcourt le dernier lambda du piquant (qui
+        contient le type de l'argument du case), et on remplace les rels
+        correspondant dans la preuve construite. *)
      
      (* typ vient du piquant, type_of_b vient du typage de b.*)
      
@@ -353,27 +411,31 @@ let rec
          [] -> c
        | ((e,e') ::l') -> substL l' (substitterm 0 e (lift 1 e') c) in
      let newpcase' = substL rel_map typeof_case'' in
+     let neweq = mkEq (lift (List.length suppllam_pcase + 1) type_of_b) 
+      (lift (List.length suppllam_pcase + 1) newb) (mkRel 1) in
      let newpcase = 
-      mkProdEg (lift (List.length suppllam_pcase + 1) type_of_b) 
-       (lift (List.length suppllam_pcase + 1) newb) (mkRel 1) 
-       newpcase' in
+      if mi.doeqs then
+        mkProd (name_of_string "eg", neweq, lift 1 newpcase') else newpcase'
+     in
      (* construction du dernier lambda du piquant. *)
      let typeof_case' = mkLambda (newname_append nme "_ind" ,typ, newpcase) in
      (* ajout des lambdas supplémentaires (type dépendant) du piquant. *)
-     let typeof_case = lamn (List.length suppllam_pcase) suppllam_pcase typeof_case' in
+     let typeof_case = 
+      lamn (List.length suppllam_pcase) suppllam_pcase typeof_case' in 
      let trm' = mkCase (cinfo,typeof_case,newb, arrPt_proof) in
-     let trm = mkApp (trm',[|(mkRefl type_of_b newb)|]) in
+     let trm = 
+      if mi.doeqs then mkApp (trm',[|(mkRefl type_of_b newb)|]) 
+      else trm' in
      trm,levar,lposeq,evararr,absc
       
   | Lambda(nme, typ, cstr) ->
-     let _, _, cconcl = destProd concl in
-     let d,f=fonc in
-     let newenv = push_rel (nme,None,typ) env in
-
+     let _, _, cconcl = destProd mi.concl in
+     let d,f=mi.fonc in
+     let newenv = push_rel (nme,None,typ) mi.env in
+     let newmi = {mi with concl=cconcl; mimick=cstr; env=newenv;
+      fonc=((if d > 0 then d+1 else 0),(if f > 0 then f+1 else 0))} in
      let rec_call,levar,lposeq,evararr,absc =
-      proofPrinc ~concl:cconcl ~absconcl:absconcl ~mimick:cstr ~env:newenv ~sigma:sigma
-      nmefonc ((if d > 0 then d+1 else 0),(if f > 0 then f+1 else 0))
-       ((mkRel 1,(nme,typ)):: lift1_lvars lst_vars)
+      proofPrinc newmi ((mkRel 1,(nme,typ)):: lift1_lvars lst_vars)
        (lift1_leqs lst_eqs) (lift1L lst_recs) in
      mkLambda (nme,typ,rec_call) , levar, lposeq,evararr,absc
 
@@ -386,34 +448,32 @@ let rec
      let varnames = List.map snd lst_vars in
      let nb_vars = (List.length varnames) in
      let nb_eqs = (List.length lst_eqs) in
-
-     (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs trouvés
-        dans les let in et les Cases. *)
+     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. *)
      (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *)
-     let terms_recs = lst_recs @ (hdMatchSub_cpl mimick fonc)  in
+     let terms_recs = lst_recs @ (hdMatchSub_cpl mi.mimick mi.fonc)  in
      
-     (*c construction du terme: application successive des variables, des appels
-       rec (mais pas des egalites), a la variable existentielle correspondant a
+     (*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. *)
-     (* d'abord, on fabrique les types des appels recursifs en replacant le nom de
-        des fonctions par les predicats dans [terms_recs]: [(f_i t u v)] devient
-        [(P_i t u v)] *)
+     (* d'abord, on fabrique les types des appels recursifs en replacant le nom
+        de des fonctions par les predicats dans [terms_recs]: [(f_i t u v)]
+        devient [(P_i t u v)] *)
      (* TODO optimiser ici: *)
-     let appsrecpred = exchange_reli_arrayi_L absconcl fonc terms_recs in
-     let typesofeqs    = eqs_of_beqs_named equality_hyp_string lst_eqs in
-     let typeofhole''' = prod_it_lift typesofeqs concl  in
-     let typeofhole''  = prod_it_anonym_lift  typeofhole''' appsrecpred in
+     let appsrecpred = exchange_reli_arrayi_L mi.absconcl mi.fonc terms_recs in
+     let typeofhole''  = prod_it_anonym_lift mi.concl appsrecpred in
      let typeofhole    = prodn nb_vars varnames typeofhole'' in
 		   
      (* Un bug de refine m'oblige à mettre ici un H (meta variable à ce point,
-        mais remplacé par H avant le refine) au lieu d'un '?', je mettrai les '?'  à
-        la fin comme ça [(([H1,H2,H3...] ...) ? ? ?)]*)
+        mais remplacé par H avant le refine) au lieu d'un '?', je mettrai les
+        '?'  à la fin comme ça [(([H1,H2,H3...] ...) ? ? ?)] *)
 
-     let newmeta = (mknewmeta()) in
+     let newmeta = mknewmeta() in
      let concl_with_var = applistc newmeta varrels in
      let conclrecs = applistc concl_with_var terms_recs in
      conclrecs,[newmeta,typeofhole], [nb_vars,(List.length terms_recs)
-      ,nb_eqs],[||],absconcl
+      ,nb_eqs],[||],mi.absconcl
 
 
 
@@ -447,16 +507,14 @@ let interp_fonc_tacarg fonctac gl =
    This function calls the big function proofPrinc. *)
 
 let invfun_proof fonc def_fonc gl_abstr pis env sigma =
- (* this counter only because of the bug of refine. [nthhyp] is
-    the number of the current hypothesis (corresponding to a ?), it
-    is used in the main  function. *)
- let _ = nthhyp := 1 in
- let princ_proof,levar,lposeq,evararr,absc =
-  proofPrinc ~concl:pis ~absconcl:gl_abstr ~mimick:def_fonc ~env:env
-   ~sigma:sigma fonc (0,0) [] [] []
- in
+ let _ = resetmeta() in
+ let mi = {concl=pis; absconcl=gl_abstr; mimick=def_fonc; env=env;
+ sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true} in
+ let princ_proof,levar,lposeq,evararr,absc = proofPrinc mi [] [] [] in
  princ_proof,levar,lposeq,evararr,absc
-  
+
+(* Do intros [i] times, then do rewrite on all introduced hyps which are called
+   ["_eq_xx"], FIX: have another filter than the name. *)
 let rec iterintro i = 
  if i<=0 then tclIDTAC else 
    tclTHEN
@@ -464,8 +522,26 @@ let rec iterintro i =
      intro
      (iterintro (i-1)))
     (fun gl -> 
-     (tclREPEAT (tclNTH_HYP i rewriteLR)) gl)
+     (tclREPEAT 
+      (tclNTH_HYP i
+       (fun hyp -> 
+        let hypname = (string_of_id (destVar hyp)) in
+        let sub = 
+         try String.sub hypname 0 4 with _ -> "" (* different than "_eq_" *) in
+        if sub="_eq_" then rewriteLR hyp else tclFAIL 0)
+      )) gl)
+
 
+(* 
+       (fun hyp gl -> 
+        let _ = print_string ("nthhyp= "^ string_of_int i) in
+        if isConst hyp && ((name_of_const hyp)=="_eq_") then
+          let _ = print_string "YES\n" in
+          rewriteLR hyp gl 
+        else 
+          let _ = print_string "NO\n" in
+          tclIDTAC gl)
+ *)
     
 (* [invfun_basic C listargs_ids gl dorew lposeq] builds the tactic
    which:
@@ -477,31 +553,26 @@ let rec iterintro i =
    \end{itemize}
 *)
 
-
 let invfun_basic open_princ_proof_applied listargs_ids gl dorew lposeq =
  (tclTHEN_i
   (tclTHEN
    (tclTHEN
     (* Refine on the right term (following the sheme of the
        given function) *)
-    (fun gl -> 
-				 refine open_princ_proof_applied  gl)
+    (fun gl -> refine open_princ_proof_applied  gl)
     (* Clear the hypothesis given as arguments of the tactic
        (because they are generalized) *)
-    (tclTHEN (fun gl -> (simpl_in_concl gl)) (tclTRY (clear listargs_ids))))
+    (tclTHEN simpl_in_concl (tclTRY (clear listargs_ids))))
    (* Now we introduce the created hypothesis, and try rewrite on
       equalities due to case analysis *)
    (fun gl ->  (tclIDTAC gl)))
 		(fun i gl -> 
    if not dorew then tclIDTAC gl
    else
-     (* d,m,f correspond respectivelyto vars, induction hyps and
+     (* d,m,f correspond respectively to vars, induction hyps and
         equalities*)
-     let d,m,f=(List.nth lposeq (i-1)) in
-     tclTHEN 
-      (tclDO d intro)
-      (tclTHEN (tclDO m intro) (iterintro f))
-      gl)
+     let d,m,f = List.nth lposeq (i-1) in
+     tclTHEN (iterintro (d)) (tclDO m (tclTRY intro)) gl)
  )
  gl
 
@@ -542,7 +613,7 @@ let invfun c l dorew gl =
     \item [def_fonc] = body of the function, where let ins have
     been expanded. *)
  let fonc, def_fonc' = interp_fonc_tacarg c gl in
- let def_fonc'',listargs' =  
+ let def_fonc'',listargs' = 
   applistc_iota def_fonc' l (pf_env gl) (project gl)  in
  let def_fonc = expand_letins def_fonc'' in
  (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *)
@@ -555,17 +626,18 @@ let invfun c l dorew gl =
   invfun_proof [|fonc|] def_fonc [||] pis (pf_env gl) (project gl) in
  (* We do not consider mutual fixpt here *)
  let princ_proof_applied = applistc princ_proof listargs' in
- let princ_applied_hyps' = 
-  patternify (List.rev levar) 
-   princ_proof_applied (Name (id_of_string "Hyp"))  in
+ let princ_applied_hyps' = patternify (List.rev levar) 
+  princ_proof_applied (Name (id_of_string "Hyp"))  in
  let princ_applied_hyps = 
   if Array.length evararr > 0 then (* Fixpoint? *)
     substit_red 0 (evararr.(0)) gl_abstr princ_applied_hyps'
   else princ_applied_hyps' (* No Fixpoint *) in
+(* let _ = prconstr princ_applied_hyps' in *)
  let princ_applied_evars = apply_levars princ_applied_hyps levar in
  let open_princ_proof_applied = princ_applied_evars in
  let listargs_ids = List.map destVar (List.filter isVar listargs') in
- invfun_basic (mkevarmap_aux open_princ_proof_applied) listargs_ids gl dorew lposeq
+ invfun_basic (mkevarmap_aux open_princ_proof_applied) listargs_ids 
+  gl dorew lposeq
 
 (* function must be a constant, all arguments must be given. *)
 let invfun_verif c l dorew gl =
@@ -574,15 +646,14 @@ let invfun_verif c l dorew gl =
    let x,_ = decompose_prod (pf_type_of gl c) in
    if List.length x = List.length l then 
      try invfun c l dorew gl
-     with _ -> 
-      error 
-      ( "Tactic went wrong for some reason. If the function you used to define\n"
-      ^ "the induction principle do not deal with dependent typed, please report.")
+     with 
+        UserError (x,y) -> raise (UserError (x,y))
    else error "wrong number of arguments for the function"
 
 
 TACTIC EXTEND FunctionalInduction
-  [ "Functional" "Induction" constr(c)  ne_constr_list(l) ] -> [ invfun_verif c l true ]
+  [ "Functional" "Induction" constr(c)  ne_constr_list(l) ] 
+     -> [ invfun_verif c l true ]
 END
 
 
@@ -607,13 +678,13 @@ let buildFunscheme fonc mutflist =
     princ_replace_metas ev abs (i+1)
      (mkLambda (
       (Name (id_of_string ("Q"^(string_of_int i)))),
-      prod_change_concl (lift 1 abs.(i)) mkProp,
+      prod_change_concl (lift 1 abs.(i)) mkthesort,
       (substitterm 0 ev.(i) (mkRel (1)) (lift 1 t))))
  in
  if Array.length evararr = 0 (* Is there a Fixpoint? *)
 	then (* No Fixpoint *)
 		 (mkLambda ((Name (id_of_string ("Q"))), 
-		 prod_change_concl ftyp mkProp,
+		 prod_change_concl ftyp mkthesort,
    (substitterm 0 gl (mkRel 1) princ_proof_hyps)))
 	else
    princ_replace_metas evararr absc 0 princ_proof_hyps
@@ -621,8 +692,11 @@ 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 scheme = 
+   buildFunscheme (constr_of f) 
+    (Array.of_list (List.map constr_of (f::mutflist))) in
+  let _ = prstr "Principe:" in
+  let _ = prconstr scheme in
  let ce = { 
   const_entry_body = scheme;
   const_entry_type = None;
@@ -655,7 +729,7 @@ END
 *** tuareg-try-indent:1 ***
 *** tuareg-with-indent:1 ***
 *** tuareg-if-then-else-inden:1 ***
-*** fill-column: 88 ***
+*** fill-column: 78 ***
 *** indent-tabs-mode: nil ***
 *** End: ***
 *)
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index d90b064193..4a8ccef819 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -18,6 +18,31 @@ open Sign
 open Reductionops
 (*i*)
 
+(*s printing of constr -- debugging *)
+
+let msg x = () (* comment this to see debugging msgs *)
+let prconstr c =  msg (str"  " ++ prterm c ++ str"\n")
+let prlistconstr lc = List.iter prconstr lc
+let prstr s = msg(str s)
+
+let prchr () = msg (str" (ret) \n")
+let prNamedConstr s c = 
+  begin
+    msg(str "");
+    msg(str(s^"==>\n  ") ++ prterm c ++ str "\n<==\n");
+    msg(str "");
+  end
+
+let prNamedLConstr_aux lc = 
+  List.map (prNamedConstr "#>") lc
+
+let prNamedLConstr s lc = 
+  begin
+    prstr s;
+    prNamedLConstr_aux lc
+  end
+
+
 (* FIXME: ref 1, pas bon, si? *)
 let evarcpt = ref 0
 let metacpt = ref 0
@@ -27,12 +52,16 @@ let mknewexist ()=
     !evarcpt,[||]
   end
 
+let resetexist ()= evarcpt := 0
+
 let mknewmeta ()= 
   begin
     metacpt := !metacpt+1;
     mkMeta !metacpt
   end
 
+let resetmeta () = metacpt := 0
+
 let  rec mkevarmap_from_listex lex =
   match lex with
 	 | [] -> Evd.empty
@@ -43,35 +72,23 @@ let  rec mkevarmap_from_listex lex =
 			 evar_body = Evar_empty} in
 		  Evd.add (mkevarmap_from_listex lex') ex info
 
-(*s printing of constr *)
-
-let prconstr c =  msg(str"  " ++ prterm c ++ str"\n")
-let prlistconstr lc = List.iter prconstr lc
-let prstr s = msg(str s)
 
-let prchr () = msg (str" (ret) \n")
-let prNamedConstr s c = 
-  begin
-    msg(str "");
-    msg(str(s^"==>\n  ") ++ prterm c ++ str "\n<==\n");
-    msg(str "");
-  end
-
-let prNamedLConstr_aux lc = 
-  List.map (prNamedConstr "#>") lc
-
-let prNamedLConstr s lc = 
-  begin
-    prstr s;
-    prNamedLConstr_aux lc
-  end
 
-let constant =Coqlib.gen_constant "Funind"
+(* tire de const\_omega.ml *)
+let constant dir s =
+  try
+    Declare.global_absolute_reference
+      (Libnames.make_path
+        (Names.make_dirpath (List.map Names.id_of_string (List.rev dir)))
+        (Names.id_of_string s))
+  with e -> print_endline (String.concat "." dir); print_endline s; 
+            raise e
+(* fin const\_omega.ml *)
 
 let mkEq typ c1 c2 = 
   mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|])
 let mkRefl typ c1 = 
-  mkApp ((constant ["Init"; "Logic"] "refl_equal"),
+  mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"),
          [| typ; c1|])
 
 let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
@@ -106,7 +123,7 @@ let rec substitterm prof t by_t in_u =
 
 
 let apply_eqtrpl eq t =
-  let tb,b,by_t = eq in
+  let r,(tb,b,by_t) = eq in
   substitterm 0 b by_t t
 
 let apply_eqtrpl_lt lt eq =  List.map (apply_eqtrpl eq) lt
@@ -123,10 +140,10 @@ let apply_refl_term eq t =
 
 let apply_eq_leqtrpl leq eq =
   List.map 
-    (function (tb,b,t) 
-	-> tb,
-	(if isRel b then b else (apply_refl_term eq b)),
-	apply_refl_term eq t) leq
+    (function (r,(tb,b,t)) ->
+		r,(tb, 
+		(if isRel b then b else (apply_refl_term eq b)), apply_refl_term eq t))
+	 leq
 
 
 
@@ -150,7 +167,8 @@ let prod_it_lift ini lcpl =
 let prod_it_anonym_lift trm lst = List.fold_right mkArrow_lift lst trm
 
 let lam_it_anonymous trm lst =
-  List.fold_right (fun elt res -> mkLambda(Name(id_of_string "Hrec"),elt,res)) lst trm
+  List.fold_right 
+	 (fun elt res -> mkLambda(Name(id_of_string "Hrec"),elt,res)) lst trm
 
 let lambda_id id typeofid cstr =
   let cstr' = mkNamedLambda (id_of_string "FUNX") typeofid cstr in
@@ -173,7 +191,7 @@ let nth_dep_constructor indtype n =
   build_dependent_constructor cstr_sum,  cstr_sum.cs_nargs
 
 
-let coq_refl_equal = lazy(constant ["Init"; "Logic"] "refl_equal")
+let coq_refl_equal = lazy(constant ["Coq"; "Init"; "Logic"] "refl_equal")
 
 let rec buildrefl_from_eqs eqs = 
   match eqs with 
@@ -222,15 +240,18 @@ let rec substit_red prof t by_t 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). *)
+(* [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 exchange_reli_arrayi_L tarr (d,f) = List.map (exchange_reli_arrayi tarr (d,f))
+let exchange_reli_arrayi_L tarr (d,f) = 
+  List.map (exchange_reli_arrayi tarr (d,f))
 
 
+(* expand all letins in a term, before building the principle. *)
 let rec expand_letins mimick =
   match kind_of_term mimick with
     | LetIn(nme,cstr1, typ, cstr) ->
@@ -239,7 +260,7 @@ let rec expand_letins mimick =
     | x -> map_constr expand_letins mimick
 	  
 
-(* From Antonia: Valeur d'une constante *)
+(* Valeur d'une constante, or identity *)
 let def_of_const t =
   match kind_of_term t with
     | Const sp -> 
@@ -250,17 +271,18 @@ let def_of_const t =
 			 with _ -> assert false)
     | _ -> t
 
-(* nom d'une constante.*)
+(* nom d'une constante. Must be a constante. x*)
 let name_of_const t =
     match (kind_of_term t) with
-      Const cst -> string_of_kn cst
-     |_ -> assert false
+        Const cst -> Names.string_of_label (Names.label cst)
+		|_ -> assert false
  ;;
 
 
 (*i
- Local Variables:
- compile-command: "make -k tacinvutils.cmo"
+  Local Variables:
+  compile-command: "make -k tacinvutils.cmo"
+  test-command: "../../bin/coqtop -q -batch -load-vernac-source ../../test-suite/success/Funind.v"
  End:
 i*)
 
diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli
index 21e3513719..b421828901 100644
--- a/contrib/funind/tacinvutils.mli
+++ b/contrib/funind/tacinvutils.mli
@@ -21,7 +21,7 @@ open Refine
 open Evd
 (*i*)
 
-(* printing *)
+(* printing debugging *)
 val prconstr: constr -> unit
 val prlistconstr: constr list  -> unit
 val prstr: string -> unit 
@@ -29,6 +29,8 @@ val prstr: string -> unit
 
 val mknewmeta: unit -> constr
 val mknewexist: unit -> existential
+val resetmeta: unit -> unit (* safe *)
+val resetexist: unit -> unit (* be careful with this one *)
 val mkevarmap_from_listex: (Term.existential * Term.types) list -> evar_map
 val mkEq: types -> constr -> constr -> constr
 (* let mkEq typ c1 c2 =   mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) *)
@@ -50,12 +52,12 @@ val prod_id: constr -> constr -> constr -> constr
 val name_of_string : string -> name
 val newname_append: name -> string -> name
 
-val apply_eqtrpl: (constr*constr*constr) -> constr -> constr
+val apply_eqtrpl: constr*(constr*constr*constr) -> constr -> constr
 val substitterm: int -> constr -> constr -> constr -> constr
 val apply_leqtrpl_t: 
-  constr -> (constr*constr*constr) list -> constr
+  constr -> (constr*(constr*constr*constr)) list -> constr
 val apply_eq_leqtrpl: 
-  (constr*constr*constr) list -> constr -> (constr*constr*constr) list
+  (constr*(constr*constr*constr)) list -> constr -> (constr*(constr*constr*constr)) list
 (* val apply_leq_lt: constr list -> constr list -> constr list *)
 
 val hdMatchSub: constr -> constr -> constr list