Merge PR#379: Introducing evar-insensitive constrs

1 files changed, 144 insertions, 133 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3199474dde..48c0f5f04c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -2,6 +2,7 @@ open Printer
 open CErrors
 open Util
 open Term
+open EConstr
 open Vars
 open Namegen
 open Names
@@ -18,6 +19,12 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
+let local_assum (na, t) =
+  RelDecl.LocalAssum (na, EConstr.Unsafe.to_constr t)
+
+let local_def (na, b, t) =
+  RelDecl.LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
+
 (* let msgnl = Pp.msgnl *)
 
 (*
@@ -95,6 +102,7 @@ let list_chop ?(msg="") n l =
   with Failure (msg') ->
     failwith (msg ^ msg')
 
+let pop t = Vars.lift (-1) t
 
 let make_refl_eq constructor type_of_t t  =
 (*   let refl_equal_term = Lazy.force refl_equal in *)
@@ -131,16 +139,16 @@ let refine c =
 
 let thin l = Proofview.V82.of_tactic (Tactics.clear l)
 
-let eq_constr u v = eq_constr_nounivs u v
+let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v
 
-let is_trivial_eq t =
+let is_trivial_eq sigma t =
   let res =   try
     begin
-      match kind_of_term t with
-	| App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
-	    eq_constr t1 t2
-	| App(f,[|t1;a1;t2;a2|]) when eq_constr f (jmeq ())  ->
-	    eq_constr t1 t2 && eq_constr a1 a2
+      match EConstr.kind sigma t with
+	| App(f,[|_;t1;t2|]) when eq_constr sigma f (Lazy.force eq) ->
+	    eq_constr sigma t1 t2
+	| App(f,[|t1;a1;t2;a2|]) when eq_constr sigma f (jmeq ())  ->
+	    eq_constr sigma t1 t2 && eq_constr sigma a1 a2
 	| _ -> false
     end
   with e when CErrors.noncritical e -> false
@@ -148,30 +156,30 @@ let is_trivial_eq t =
 (*   observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
   res
 
-let rec incompatible_constructor_terms t1 t2 =
-  let c1,arg1 = decompose_app t1
-  and c2,arg2 = decompose_app t2
+let rec incompatible_constructor_terms sigma t1 t2 =
+  let c1,arg1 = decompose_app sigma t1
+  and c2,arg2 = decompose_app sigma t2
   in
-  (not (eq_constr t1 t2)) &&
-    isConstruct c1 && isConstruct c2 &&
+  (not (eq_constr sigma t1 t2)) &&
+    isConstruct sigma c1 && isConstruct sigma c2 &&
     (
-      not (eq_constr c1 c2) ||
-	List.exists2 incompatible_constructor_terms arg1 arg2
+      not (eq_constr sigma c1 c2) ||
+	List.exists2 (incompatible_constructor_terms sigma) arg1 arg2
     )
 
-let is_incompatible_eq t =
+let is_incompatible_eq sigma t =
   let res =
     try
-      match kind_of_term t with
-	| App(f,[|_;t1;t2|]) when eq_constr f (Lazy.force eq) ->
-	    incompatible_constructor_terms t1 t2
-	| App(f,[|u1;t1;u2;t2|]) when eq_constr f (jmeq ()) ->
-	    (eq_constr u1 u2 &&
-	       incompatible_constructor_terms t1 t2)
+      match EConstr.kind sigma t with
+	| App(f,[|_;t1;t2|]) when eq_constr sigma f (Lazy.force eq) ->
+	    incompatible_constructor_terms sigma t1 t2
+	| App(f,[|u1;t1;u2;t2|]) when eq_constr sigma f (jmeq ()) ->
+	    (eq_constr sigma u1 u2 &&
+	       incompatible_constructor_terms sigma t1 t2)
 	| _ -> false
     with e when CErrors.noncritical e -> false
   in
-  if res then   observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t);
+  if res then   observe (str "is_incompatible_eq " ++ Printer.pr_leconstr t);
   res
 
 let change_hyp_with_using msg hyp_id t tac : tactic =
@@ -208,40 +216,38 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) =
 
 
 
-let find_rectype env c =
-  let (t, l) = decompose_app (Reduction.whd_betaiotazeta env c) in
-  match kind_of_term t with
+let find_rectype env sigma c =
+  let (t, l) = decompose_app sigma (Reductionops.whd_betaiotazeta sigma c) in
+  match EConstr.kind sigma t with
   | Ind ind -> (t, l)
   | Construct _ -> (t,l)
   | _ -> raise Not_found
 
 
-let isAppConstruct ?(env=Global.env ()) t =
+let isAppConstruct ?(env=Global.env ()) sigma t =
   try
-    let t',l = find_rectype (Global.env ()) t in
-    observe (str "isAppConstruct : " ++ Printer.pr_lconstr t ++ str " -> " ++ Printer.pr_lconstr (applist  (t',l)));
+    let t',l = find_rectype env sigma t in
+    observe (str "isAppConstruct : " ++ Printer.pr_leconstr t ++ str " -> " ++ Printer.pr_leconstr (applist  (t',l)));
     true
   with Not_found -> false
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
-  let clos_norm_flags flgs env sigma t =
-    CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in
-  clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
+  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
 
 
 
-let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
+let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
   let nochange ?t' msg  =
     begin
-      observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t  ++ str "    " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t );
+      observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t  ++ str "    " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t );
       failwith "NoChange";
     end
   in
-  let eq_constr = Evarconv.e_conv env (ref sigma) in
-  if not (noccurn 1 end_of_type)
+  let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in
+  if not (noccurn sigma 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
-    if not (isApp t) then nochange "not an equality";
-    let f_eq,args = destApp t in
+    if not (isApp sigma t) then nochange "not an equality";
+    let f_eq,args = destApp sigma t in
     let constructor,t1,t2,t1_typ =
       try
 	if (eq_constr f_eq (Lazy.force eq))
@@ -258,36 +264,36 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	  else nochange "not an equality"
       with e when CErrors.noncritical e -> nochange "not an equality"
     in
-    if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs";
+    if not ((closed0 sigma (fst t1)) && (closed0 sigma (snd t1)))then nochange "not a closed lhs";
     let rec compute_substitution sub t1 t2 =
 (*       observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); *)
-      if isRel t2
+      if isRel sigma t2
       then
-	let t2 = destRel t2  in
+	let t2 = destRel sigma t2  in
 	begin
 	  try
 	    let t1' = Int.Map.find t2 sub in
 	    if not (eq_constr t1 t1') then nochange "twice bound variable";
 	    sub
 	  with Not_found ->
-	    assert (closed0 t1);
+	    assert (closed0 sigma t1);
 	    Int.Map.add t2 t1 sub
 	end
-      else if isAppConstruct t1 && isAppConstruct t2
+      else if isAppConstruct sigma t1 && isAppConstruct sigma t2
       then
 	begin
-	  let c1,args1 =  find_rectype env t1
-	  and c2,args2 = find_rectype env t2
+	  let c1,args1 =  find_rectype env sigma t1
+	  and c2,args2 = find_rectype env sigma t2
 	  in
 	  if not (eq_constr c1 c2) then nochange "cannot solve (diff)";
 	  List.fold_left2 compute_substitution sub args1 args2
 	end
       else
-	if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_all env t1) t2)  "cannot solve (diff)"
+	if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reductionops.whd_all env sigma t1) t2)  "cannot solve (diff)"
     in
     let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in
     let sub = compute_substitution sub (fst t1) (fst t2) in
-    let end_of_type_with_pop = Termops.pop end_of_type in (*the equation will be removed *)
+    let end_of_type_with_pop = pop end_of_type in (*the equation will be removed *)
     let new_end_of_type =
       (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
 	 Can be safely replaced by the next comment for Ocaml >= 3.08.4
@@ -309,7 +315,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	   try
 	     let witness = Int.Map.find i sub in
 	     if is_local_def decl then anomaly (Pp.str "can not redefine a rel!");
-	     (Termops.pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
+	     (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun))
 	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
 	)
@@ -318,9 +324,9 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	context
     in
     let new_type_of_hyp =
-      Reductionops.nf_betaiota Evd.empty new_type_of_hyp in
+      Reductionops.nf_betaiota sigma new_type_of_hyp in
     let new_ctxt,new_end_of_type =
-      decompose_prod_n_assum ctxt_size new_type_of_hyp
+      decompose_prod_n_assum sigma ctxt_size new_type_of_hyp
     in
     let prove_new_hyp : tactic =
       tclTHEN
@@ -353,21 +359,21 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
     new_ctxt,new_end_of_type,simpl_eq_tac
 
 
-let is_property (ptes_info:ptes_info) t_x full_type_of_hyp =
-  if isApp t_x
+let is_property sigma (ptes_info:ptes_info) t_x full_type_of_hyp =
+  if isApp sigma t_x
   then
-    let pte,args = destApp t_x in
-    if isVar pte && Array.for_all closed0 args
+    let pte,args = destApp sigma t_x in
+    if isVar sigma pte && Array.for_all (closed0 sigma) args
     then
       try
-	let info = Id.Map.find (destVar pte) ptes_info in
+	let info = Id.Map.find (destVar sigma pte) ptes_info in
 	info.is_valid full_type_of_hyp
       with Not_found -> false
     else false
   else false
 
-let isLetIn t =
-  match kind_of_term t with
+let isLetIn sigma t =
+  match EConstr.kind sigma t with
     | LetIn _ -> true
     | _ -> false
 
@@ -387,8 +393,9 @@ let rewrite_until_var arg_num eq_ids : tactic =
      will break the Guard when trying to save the Lemma.
   *)
   let test_var g =
-    let _,args = destApp (pf_concl g) in
-    not ((isConstruct args.(arg_num)) || isAppConstruct args.(arg_num))
+    let sigma = project g in
+    let _,args = destApp sigma (pf_concl g) in
+    not ((isConstruct sigma args.(arg_num)) || isAppConstruct sigma args.(arg_num))
   in
   let rec do_rewrite eq_ids g  =
     if test_var g
@@ -407,30 +414,30 @@ let rewrite_until_var arg_num eq_ids : tactic =
 
 let rec_pte_id = Id.of_string "Hrec"
 let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
-  let coq_False = Coqlib.build_coq_False () in
-  let coq_True = Coqlib.build_coq_True () in
-  let coq_I = Coqlib.build_coq_I () in
+  let coq_False = EConstr.of_constr (Coqlib.build_coq_False ()) in
+  let coq_True = EConstr.of_constr (Coqlib.build_coq_True ()) in
+  let coq_I = EConstr.of_constr (Coqlib.build_coq_I ()) in
   let rec scan_type  context type_of_hyp : tactic =
-    if isLetIn type_of_hyp then
+    if isLetIn sigma type_of_hyp then
       let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
       let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
       (* length of context didn't change ? *)
       let new_context,new_typ_of_hyp =
-	 decompose_prod_n_assum (List.length context) reduced_type_of_hyp
+	 decompose_prod_n_assum sigma (List.length context) reduced_type_of_hyp
       in
         tclTHENLIST
 	[ h_reduce_with_zeta (Locusops.onHyp hyp_id);
 	  scan_type new_context new_typ_of_hyp ]
-    else if isProd type_of_hyp
+    else if isProd sigma type_of_hyp
     then
       begin
-	let (x,t_x,t') = destProd type_of_hyp in
+	let (x,t_x,t') = destProd sigma type_of_hyp in
 	let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in
-	if is_property ptes_infos t_x actual_real_type_of_hyp then
+	if is_property sigma ptes_infos t_x actual_real_type_of_hyp then
 	  begin
-	    let pte,pte_args =  (destApp t_x) in
-	    let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar pte) ptes_infos).proving_tac in
-	    let popped_t' = Termops.pop t' in
+	    let pte,pte_args =  (destApp sigma t_x) in
+	    let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar sigma pte) ptes_infos).proving_tac in
+	    let popped_t' = pop t' in
 	    let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in
 	    let prove_new_type_of_hyp =
 	      let context_length = List.length context in
@@ -467,20 +474,20 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		scan_type context popped_t'
 	      ]
 	  end
-	else if eq_constr t_x coq_False then
+	else if eq_constr sigma t_x coq_False then
 	  begin
 (* 	    observe (str "Removing : "++ Ppconstr.pr_id hyp_id++  *)
 (* 		       str " since it has False in its preconds " *)
 (* 		    ); *)
 	    raise TOREMOVE;  (* False -> .. useless *)
 	  end
-	else if is_incompatible_eq t_x then raise TOREMOVE (* t_x := C1 ... =  C2 ... *)
-	else if eq_constr t_x coq_True  (* Trivial => we remove this precons *)
+	else if is_incompatible_eq sigma t_x then raise TOREMOVE (* t_x := C1 ... =  C2 ... *)
+	else if eq_constr sigma t_x coq_True  (* Trivial => we remove this precons *)
 	then
 (* 	    observe (str "In "++Ppconstr.pr_id hyp_id++  *)
 (* 		       str " removing useless precond True" *)
 (* 		    );  *)
-	  let popped_t' = Termops.pop t' in
+	  let popped_t' = pop t' in
 	  let real_type_of_hyp =
 	    it_mkProd_or_LetIn popped_t' context
 	  in
@@ -506,15 +513,15 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	      ((* observe_tac "prove_trivial" *) prove_trivial);
 	    scan_type context popped_t'
 	  ]
-	else if is_trivial_eq t_x
+	else if is_trivial_eq sigma t_x
 	then (*  t_x :=  t = t   => we remove this precond *)
-	  let popped_t' = Termops.pop t' in
+	  let popped_t' = pop t' in
 	  let real_type_of_hyp =
 	    it_mkProd_or_LetIn popped_t' context
 	  in
-	  let hd,args = destApp t_x in
+	  let hd,args = destApp sigma t_x in
 	  let get_args hd args =
-	    if eq_constr hd (Lazy.force eq)
+	    if eq_constr sigma hd (Lazy.force eq)
 	    then (Lazy.force refl_equal,args.(0),args.(1))
 	    else (jmeq_refl (),args.(0),args.(1))
 	  in
@@ -597,18 +604,18 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	   let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
 	   (* compute the new value of the body *)
 	   let new_term_value =
-	     match kind_of_term new_term_value_eq with
+	     match EConstr.kind (project g') new_term_value_eq with
 	       | App(f,[| _;_;args2 |]) -> args2
 	       | _ ->
 		   observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++
-			      pr_lconstr_env (pf_env g') Evd.empty new_term_value_eq
+			      pr_leconstr_env (pf_env g') (project g') new_term_value_eq
 			   );
 		   anomaly (Pp.str "cannot compute new term value")
 	   in
 	 let fun_body =
 	   mkLambda(Anonymous,
 		    pf_unsafe_type_of g' term,
-		    Termops.replace_term term (mkRel 1) dyn_infos.info
+		    Termops.replace_term (project g') term (mkRel 1) dyn_infos.info
 		   )
 	 in
 	 let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
@@ -691,15 +698,16 @@ let build_proof
     : tactic =
   let rec build_proof_aux do_finalize dyn_infos : tactic =
     fun g ->
+        let sigma = project g in
 (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
-	match kind_of_term dyn_infos.info with
+	match EConstr.kind sigma dyn_infos.info with
 	  | Case(ci,ct,t,cb) ->
 	      let do_finalize_t dyn_info' =
 		fun g ->
 		  let t = dyn_info'.info in
 		  let dyn_infos = {dyn_info' with info =
 		      mkCase(ci,ct,t,cb)} in
-		  let g_nb_prod = nb_prod (pf_concl g) in
+		  let g_nb_prod = nb_prod (project g) (pf_concl g) in
 		  let type_of_term = pf_unsafe_type_of g t in
 		  let term_eq =
 		    make_refl_eq (Lazy.force refl_equal) type_of_term t
@@ -712,7 +720,7 @@ let build_proof
 		      (fun g -> observe_tac "toto" (
 			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
 				     (fun g' ->
-					let g'_nb_prod = nb_prod (pf_concl g') in
+					let g'_nb_prod = nb_prod (project g') (pf_concl g') in
 					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
 			 		observe_tac "treat_new_case"
 					  (treat_new_case
@@ -732,7 +740,7 @@ let build_proof
 	      build_proof do_finalize_t {dyn_infos with info = t} g
 	  | Lambda(n,t,b) ->
 	      begin
-		match kind_of_term( pf_concl g) with
+		match EConstr.kind sigma (pf_concl g) with
 		  | Prod _ ->
 		      tclTHEN
 			(Proofview.V82.of_tactic intro)
@@ -762,9 +770,9 @@ let build_proof
 	  | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
 	      do_finalize dyn_infos g
 	  | App(_,_) ->
-	      let f,args = decompose_app dyn_infos.info in
+	      let f,args = decompose_app sigma dyn_infos.info in
 	      begin
-		match kind_of_term f with
+		match EConstr.kind sigma f with
 		  | App _ -> assert false (* we have collected all the app in decompose_app *)
 		  | Proj _ -> assert false (*FIXME*)
 		  | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ | Sort _ | Prod _ ->
@@ -786,7 +794,7 @@ let build_proof
 		      do_finalize dyn_infos  g
 		  | Lambda _ ->
 		      let new_term =
-                        Reductionops.nf_beta Evd.empty dyn_infos.info in
+                        Reductionops.nf_beta sigma dyn_infos.info in
 		      build_proof do_finalize {dyn_infos with info = new_term}
 			g
 		  | LetIn _ ->
@@ -838,7 +846,7 @@ let build_proof
 	  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
-    observe_tac_stream (str "build_proof with " ++ Printer.pr_lconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
+    observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
   and build_proof_args do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
       let (f_args',args) = dyn_infos.info in
@@ -904,7 +912,7 @@ let prove_rec_hyp_for_struct fix_info =
       (fun  eq_hyps -> tclTHEN
 	(rewrite_until_var (fix_info.idx) eq_hyps)
 	(fun g ->
-	   let _,pte_args = destApp (pf_concl g) in
+	   let _,pte_args = destApp (project g) (pf_concl g) in
 	   let rec_hyp_proof =
 	     mkApp(mkVar fix_info.name,array_get_start pte_args)
 	   in
@@ -925,10 +933,11 @@ let generalize_non_dep hyp g =
   let to_revert,_ =
     let open Context.Named.Declaration in
     Environ.fold_named_context_reverse (fun (clear,keep) decl ->
+      let decl = map_named_decl EConstr.of_constr decl in
       let hyp = get_id decl in
       if Id.List.mem hyp hyps
-        || List.exists (Termops.occur_var_in_decl env hyp) keep
-	|| Termops.occur_var env hyp hyp_typ
+        || List.exists (Termops.occur_var_in_decl env (project g) hyp) keep
+	|| Termops.occur_var env (project g) hyp hyp_typ
 	|| Termops.is_section_variable hyp (* should be dangerous *)
       then (clear,decl::keep)
       else (hyp::clear,keep))
@@ -951,11 +960,12 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 (*   observe (str "nb_args := " ++ str (string_of_int nb_args)); *)
 (*   observe (str "nb_params := " ++ str (string_of_int nb_params)); *)
 (*   observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
-  let f_def = Global.lookup_constant (fst (destConst f)) in
+  let f_def = Global.lookup_constant (fst (destConst evd f)) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
   let f_body = Option.get (Global.body_of_constant_body f_def) in
-  let params,f_body_with_params = decompose_lam_n nb_params f_body in
-  let (_,num),(_,_,bodies) = destFix f_body_with_params in
+  let f_body = EConstr.of_constr f_body in
+  let params,f_body_with_params = decompose_lam_n evd nb_params f_body in
+  let (_,num),(_,_,bodies) = destFix evd f_body_with_params in
   let fnames_with_params =
     let params = Array.init nb_params (fun i -> mkRel(nb_params - i)) in
     let fnames = List.rev (Array.to_list (Array.map (fun f -> mkApp(f,params)) fnames)) in
@@ -970,13 +980,13 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let (type_ctxt,type_of_f),evd =
     let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
     in 
-    decompose_prod_n_assum
+    decompose_prod_n_assum evd
       (nb_params + nb_args) t,evd
   in
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
   let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
   (* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *)
-  let f_id = Label.to_id (con_label (fst (destConst f))) in
+  let f_id = Label.to_id (con_label (fst (destConst evd f))) in
   let prove_replacement =
     tclTHENSEQ
       [
@@ -1010,10 +1020,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
   let equation_lemma =
     try
-      let finfos = find_Function_infos (fst (destConst f)) (*FIXME*) in
+      let finfos = find_Function_infos (fst (destConst !evd f)) (*FIXME*) in
       mkConst (Option.get finfos.equation_lemma)
     with (Not_found | Option.IsNone as e) ->
-      let f_id = Label.to_id (con_label (fst (destConst f))) in
+      let f_id = Label.to_id (con_label (fst (destConst !evd f))) in
       (*i The next call to mk_equation_id is valid since we will construct the lemma
 	Ensures by: obvious
 	i*)
@@ -1022,7 +1032,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
       let _ =
 	match e with
 	  | Option.IsNone ->
-	      let finfos = find_Function_infos (fst (destConst f)) in
+	      let finfos = find_Function_infos (fst (destConst !evd f)) in
 	      update_Function
 		{finfos with
 		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
@@ -1038,11 +1048,12 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	  (Global.env ()) !evd
 	  (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
       in
+      let res = EConstr.of_constr res in
       evd:=evd';                       
       let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
       res
   in
-  let nb_intro_to_do = nb_prod (pf_concl g) in
+  let nb_intro_to_do = nb_prod (project g) (pf_concl g) in
     tclTHEN
       (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro))
       (
@@ -1061,7 +1072,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
   (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *)
   (* Pp.msgnl (str "all_funs "); *)
   (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *)
-    let princ_info = compute_elim_sig princ_type in
+    let princ_info = compute_elim_sig (project g) princ_type in
     let fresh_id =
       let avoid = ref (pf_ids_of_hyps g) in
       (fun na ->
@@ -1090,11 +1101,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	       (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	       (Global.env ())
 	       (Evd.empty)
-	       body
+	       (EConstr.of_constr body)
 	| None -> error ( "Cannot define a principle over an axiom ")
     in
     let fbody = get_body fnames.(fun_num) in
-    let f_ctxt,f_body = decompose_lam fbody in
+    let f_ctxt,f_body = decompose_lam (project g) fbody in
     let f_ctxt_length = List.length f_ctxt in
     let diff_params = princ_info.nparams - f_ctxt_length in
     let full_params,princ_params,fbody_with_full_params =
@@ -1129,19 +1140,19 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	       princ_params
 	    );
     observe (str "fbody_with_full_params := " ++
-	       pr_lconstr fbody_with_full_params
+	       pr_leconstr fbody_with_full_params
 	    );
     let all_funs_with_full_params =
       Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
     in
     let fix_offset = List.length princ_params in
     let ptes_to_fix,infos =
-      match kind_of_term fbody_with_full_params with
+      match EConstr.kind (project g) fbody_with_full_params with
 	| Fix((idxs,i),(names,typess,bodies)) ->
 	    let bodies_with_all_params =
 	      Array.map
 		(fun body ->
-		   Reductionops.nf_betaiota Evd.empty
+		   Reductionops.nf_betaiota (project g)
 		     (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
 			      List.rev_map var_of_decl princ_params))
 		)
@@ -1150,14 +1161,14 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    let info_array =
 	      Array.mapi
 		(fun i types ->
-		   let types = prod_applist types (List.rev_map var_of_decl princ_params) in
+		   let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in
 		   { idx = idxs.(i)  - fix_offset;
 		     name = Nameops.out_name (fresh_id names.(i));
 		     types = types;
 		     offset = fix_offset;
 		     nb_realargs =
 		       List.length
-			 (fst (decompose_lam bodies.(i))) - fix_offset;
+			 (fst (decompose_lam (project g) bodies.(i))) - fix_offset;
 		     body_with_param = bodies_with_all_params.(i);
 		     num_in_block = i
 		   }
@@ -1169,7 +1180,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		(fun i (acc_map,acc_info) decl ->
 		   let pte = RelDecl.get_name decl in
 		   let infos = info_array.(i) in
-		   let type_args,_ = decompose_prod infos.types in
+		   let type_args,_ = decompose_prod (project g) infos.types in
 		   let nargs = List.length type_args in
 		   let f = applist(mkConst fnames.(i), List.rev_map var_of_decl princ_info.params) in
 		   let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in
@@ -1179,12 +1190,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		   let body_with_param,num =
 		     let body = get_body fnames.(i) in
 		     let body_with_full_params =
-		       Reductionops.nf_betaiota Evd.empty (
+		       Reductionops.nf_betaiota (project g) (
 			 applist(body,List.rev_map var_of_decl full_params))
 		     in
-		     match kind_of_term body_with_full_params with
+		     match EConstr.kind (project g) body_with_full_params with
 		       | Fix((_,num),(_,_,bs)) ->
-			       Reductionops.nf_betaiota Evd.empty
+			       Reductionops.nf_betaiota (project g)
 				 (
 				   (applist
 				      (substl
@@ -1244,11 +1255,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
     in
     let intros_after_fixes : tactic =
       fun gl ->
-	let ctxt,pte_app =  (decompose_prod_assum (pf_concl gl)) in
-	let pte,pte_args = (decompose_app pte_app) in
+	let ctxt,pte_app =  (decompose_prod_assum (project gl) (pf_concl gl)) in
+	let pte,pte_args = (decompose_app (project gl) pte_app) in
 	try
 	  let pte =
-            try destVar pte
+            try destVar (project gl) pte
             with DestKO -> anomaly (Pp.str "Property is not a variable")
           in
 	  let fix_info = Id.Map.find  pte ptes_to_fix in
@@ -1267,7 +1278,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-		       Reductionops.nf_betaiota Evd.empty
+		       Reductionops.nf_betaiota (project g)
 			 (applist(fix_body,List.rev_map mkVar args_id));
 		     eq_hyps = []
 		   }
@@ -1335,7 +1346,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     eq_hyps = []
 		   }
 		 in
-		 let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
+		 let fname = destConst (project g) (fst (decompose_app (project g) (List.hd (List.rev pte_args)))) in
 		 tclTHENSEQ
 		   [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]);
 		    let do_prove =
@@ -1417,14 +1428,14 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
     let rewrite =
       tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
     in
-    let _,hrec_concl  = decompose_prod (pf_unsafe_type_of gls (mkVar hrec)) in
-    let f_app = Array.last (snd (destApp hrec_concl)) in
-    let f =  (fst (destApp f_app)) in
+    let _,hrec_concl  = decompose_prod (project gls) (pf_unsafe_type_of gls (mkVar hrec)) in
+    let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in
+    let f =  (fst (destApp (project gls) f_app)) in
     let rec backtrack : tactic =
       fun g ->
-	let f_app = Array.last (snd (destApp (pf_concl g))) in
-	match kind_of_term f_app with
-	  | App(f',_) when eq_constr f' f -> tclIDTAC g
+	let f_app = Array.last (snd (destApp (project g) (pf_concl g))) in
+	match EConstr.kind (project g) f_app with
+	  | App(f',_) when eq_constr (project g) f' f -> tclIDTAC g
 	  | _ -> tclTHEN rewrite backtrack g
     in
     backtrack gls
@@ -1488,20 +1499,20 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
       gls
 
 
-let is_valid_hypothesis predicates_name =
+let is_valid_hypothesis sigma predicates_name =
   let predicates_name = List.fold_right Id.Set.add predicates_name Id.Set.empty in
   let is_pte typ =
-    if isApp typ
+    if isApp sigma typ
     then
-      let pte,_ = destApp typ in
-      if isVar pte
-      then Id.Set.mem (destVar pte) predicates_name
+      let pte,_ = destApp sigma typ in
+      if isVar sigma pte
+      then Id.Set.mem (destVar sigma pte) predicates_name
       else false
     else false
   in
   let rec is_valid_hypothesis typ =
     is_pte typ ||
-      match kind_of_term typ with
+      match EConstr.kind sigma typ with
 	| Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ'
 	| _ -> false
   in
@@ -1511,7 +1522,7 @@ let prove_principle_for_gen
     (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
     rec_arg_num rec_arg_type relation gl =
   let princ_type = pf_concl gl in
-  let princ_info = compute_elim_sig princ_type in
+  let princ_info = compute_elim_sig (project gl) princ_type in
   let fresh_id =
     let avoid = ref (pf_ids_of_hyps gl) in
     fun na ->
@@ -1589,7 +1600,7 @@ let prove_principle_for_gen
   let lemma =
     match !tcc_lemma_ref with
      | None -> error "No tcc proof !!"
-     | Some lemma -> lemma
+     | Some lemma -> EConstr.of_constr lemma
   in
 (*   let rec list_diff del_list check_list = *)
 (*     match del_list with *)
@@ -1649,7 +1660,7 @@ let prove_principle_for_gen
       Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
       (* observe_tac "finish" *) (fun gl' ->
 	 let body =
-	   let _,args = destApp (pf_concl gl') in
+	   let _,args = destApp (project gl') (pf_concl gl') in
 	   Array.last args
 	 in
 	 let body_info rec_hyps =
@@ -1692,7 +1703,7 @@ let prove_principle_for_gen
 		    )
 
 	       );
-	     is_valid = is_valid_hypothesis predicates_names
+	     is_valid = is_valid_hypothesis (project gl') predicates_names
 	   }
 	 in
 	 let ptes_info : pte_info Id.Map.t =