Funind API using EConstr.

15 files changed, 579 insertions, 495 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c98cdc467..656924e38 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 *)
 
 (*
@@ -132,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
@@ -149,34 +156,33 @@ 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 =
-  let t = EConstr.of_constr t in
   fun g ->
     let prov_id = pf_get_new_id hyp_id g in
     tclTHENS
@@ -204,47 +210,44 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) =
 	     (List.map mkVar context_hyps)
 	 in
 	 let to_refine = applist(mkVar h_id,List.rev context_hyps') in
-	 let to_refine = EConstr.of_constr to_refine in
 	 refine to_refine g
       )
     ]
 
 
 
-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 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 c1 c2 = Evarconv.e_conv env (ref sigma) (EConstr.of_constr c1) (EConstr.of_constr c2) 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))
@@ -261,32 +264,32 @@ 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
@@ -312,19 +315,18 @@ 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!");
-	     (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, EConstr.of_constr (RelDecl.get_type decl), witness_fun))
 	   with Not_found  ->
-	     (Term.mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
+	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
 	)
 	1
 	(new_end_of_type,0,witness_fun)
 	context
     in
     let new_type_of_hyp =
-      Reductionops.nf_betaiota Evd.empty (EConstr.of_constr new_type_of_hyp) in
-    let new_type_of_hyp = EConstr.Unsafe.to_constr 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
@@ -333,7 +335,6 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	   let all_ids = pf_ids_of_hyps g in
 	   let new_ids,_  = list_chop ctxt_size all_ids in
 	   let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
-	   let to_refine = EConstr.of_constr to_refine in
 	   let evm, _ = pf_apply Typing.type_of g to_refine in
 	     tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
 	)
@@ -358,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
 
@@ -392,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 (EConstr.of_constr (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
@@ -403,7 +405,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
 	| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
 	| eq_id::eq_ids ->
 	    tclTHEN
-	      (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar eq_id))))
+	      (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id))))
 	      (do_rewrite eq_ids)
 	      g
   in
@@ -412,31 +414,31 @@ 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
-      let real_type_of_hyp = Term.it_mkProd_or_LetIn type_of_hyp context in
+    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 actual_real_type_of_hyp = Term.it_mkProd_or_LetIn t' context in
-	if is_property ptes_infos t_x actual_real_type_of_hyp then
+	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 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 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 = Term.it_mkProd_or_LetIn popped_t' context 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
 	      tclTHENLIST
@@ -453,8 +455,6 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 			       List.rev_map mkVar (rec_pte_id::context_hyps_ids)
 			      )
 		     in
-		     let to_refine = EConstr.of_constr to_refine in
-		     let t_x = EConstr.of_constr t_x in
 (* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
 		       (Proofview.V82.of_tactic (assert_before (Name rec_pte_id) t_x))
@@ -474,22 +474,22 @@ 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' = pop t' in
 	  let real_type_of_hyp =
-	    Term.it_mkProd_or_LetIn popped_t' context
+	    it_mkProd_or_LetIn popped_t' context
 	  in
 	  let prove_trivial =
 	    let nb_intro = List.length context in
@@ -504,7 +504,6 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 			    List.rev (coq_I::List.map mkVar context_hyps)
 			   )
 		 in
-		 let to_refine = (EConstr.of_constr to_refine) in
 		 refine to_refine g
 	      )
 	    ]
@@ -514,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' = pop t' in
 	  let real_type_of_hyp =
-	    Term.it_mkProd_or_LetIn popped_t' context
+	    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
@@ -545,14 +544,14 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		(scan_type new_context new_t')
 	    with Failure "NoChange" ->
 	      (* Last thing todo : push the rel in the context and continue *)
-	      scan_type (LocalAssum (x,t_x) :: context) t'
+	      scan_type (local_assum (x,t_x) :: context) t'
 	  end
       end
     else
       tclIDTAC
   in
   try
-    scan_type [] (Typing.unsafe_type_of env sigma (EConstr.mkVar hyp_id)), [hyp_id]
+    scan_type [] (EConstr.of_constr (Typing.unsafe_type_of env sigma (mkVar hyp_id))), [hyp_id]
   with TOREMOVE ->
     thin [hyp_id],[]
 
@@ -602,26 +601,25 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
 	observe_tac "after_introduction" (fun g' ->
 	   (* We get infos on the equations introduced*)
-	   let new_term_value_eq = pf_unsafe_type_of g' (EConstr.mkVar heq_id) in
+	   let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
+	   let new_term_value_eq = EConstr.of_constr new_term_value_eq 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 term = EConstr.of_constr term in
 	 let fun_body =
 	   mkLambda(Anonymous,
-		    pf_unsafe_type_of g' term,
-		    EConstr.Unsafe.to_constr (Termops.replace_term (project g') term (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info)
-		   ))
+		    EConstr.of_constr (pf_unsafe_type_of g' term),
+		    Termops.replace_term (project g') term (mkRel 1) dyn_infos.info
+		   )
 	 in
-	 let new_body = pf_nf_betaiota g' (EConstr.of_constr (mkApp(fun_body,[| new_term_value |]))) in
-	 let new_body = EConstr.Unsafe.to_constr new_body in
+	 let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
 	 let new_infos =
 	   {dyn_infos with
 	      info = new_body;
@@ -649,7 +647,6 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 	fun g ->
 	  let prov_hid = pf_get_new_id hid g in
 	  let c = mkApp(mkVar hid,args) in
-	  let c = EConstr.of_constr c in
 	  let evm, _ = pf_apply Typing.type_of g c in
 	  tclTHENLIST[
             Refiner.tclEVARS evm;
@@ -702,8 +699,9 @@ 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 ->
@@ -711,18 +709,18 @@ let build_proof
 		  let dyn_infos = {dyn_info' with info =
 		      mkCase(ci,ct,t,cb)} in
 		  let g_nb_prod = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in
-		  let type_of_term = pf_unsafe_type_of g (EConstr.of_constr t) in
+		  let type_of_term = pf_unsafe_type_of g t in
+		  let type_of_term = EConstr.of_constr type_of_term in
 		  let term_eq =
 		    make_refl_eq (Lazy.force refl_equal) type_of_term t
 		  in
-		  let term_eq = EConstr.of_constr term_eq in
 		  tclTHENSEQ
 		    [
-		      Proofview.V82.of_tactic (generalize (term_eq::(List.map EConstr.mkVar dyn_infos.rec_hyps)));
+		      Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)));
 		      thin dyn_infos.rec_hyps;
-		      Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],EConstr.of_constr t] None);
+		      Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
 		      (fun g -> observe_tac "toto" (
-			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case (EConstr.of_constr t));
+			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
 				     (fun g' ->
 					let g'_nb_prod = nb_prod (project g') (EConstr.of_constr (pf_concl g')) in
 					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
@@ -744,7 +742,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 (EConstr.of_constr ( pf_concl g)) with
 		  | Prod _ ->
 		      tclTHEN
 			(Proofview.V82.of_tactic intro)
@@ -753,9 +751,8 @@ let build_proof
 			   let id = pf_last_hyp g' |> get_id in
 			   let new_term =
 			     pf_nf_betaiota g'
-			       (EConstr.of_constr (mkApp(dyn_infos.info,[|mkVar id|])))
+			       (mkApp(dyn_infos.info,[|mkVar id|]))
 			   in
-			   let new_term = EConstr.Unsafe.to_constr new_term in
 			   let new_infos = {dyn_infos with info = new_term} in
 			   let do_prove new_hyps =
 			     build_proof do_finalize
@@ -775,9 +772,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 _ ->
@@ -799,8 +796,7 @@ let build_proof
 		      do_finalize dyn_infos  g
 		  | Lambda _ ->
 		      let new_term =
-                        Reductionops.nf_beta Evd.empty (EConstr.of_constr dyn_infos.info) in
-                      let new_term = EConstr.Unsafe.to_constr new_term in
+                        Reductionops.nf_beta sigma dyn_infos.info in
 		      build_proof do_finalize {dyn_infos with info = new_term}
 			g
 		  | LetIn _ ->
@@ -852,7 +848,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
@@ -918,11 +914,10 @@ 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) (EConstr.of_constr (pf_concl g)) in
 	   let rec_hyp_proof =
 	     mkApp(mkVar fix_info.name,array_get_start pte_args)
 	   in
-	   let rec_hyp_proof = EConstr.of_constr rec_hyp_proof in
 	   refine rec_hyp_proof g
 	))
 
@@ -936,7 +931,7 @@ let generalize_non_dep hyp g =
 (*   observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
   let hyps = [hyp] in
   let env = Global.env () in
-  let hyp_typ = pf_unsafe_type_of g (EConstr.mkVar hyp) in
+  let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in
   let to_revert,_ =
     let open Context.Named.Declaration in
     Environ.fold_named_context_reverse (fun (clear,keep) decl ->
@@ -951,7 +946,7 @@ let generalize_non_dep hyp g =
   in
 (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
   tclTHEN
-    ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize  (List.map EConstr.mkVar to_revert) )))
+    ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize  (List.map mkVar to_revert) )))
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
@@ -959,18 +954,19 @@ let id_of_decl = RelDecl.get_name %> Nameops.out_name
 let var_of_decl = id_of_decl %> mkVar
 let revert idl =
   tclTHEN
-    (Proofview.V82.of_tactic (generalize (List.map EConstr.mkVar idl)))
+    (Proofview.V82.of_tactic (generalize (List.map mkVar idl)))
     (thin idl)
 
 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
@@ -983,16 +979,15 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
   (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
   let (type_ctxt,type_of_f),evd =
-    let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f)
+    let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
     in 
-    let t = EConstr.Unsafe.to_constr t 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 = Term.it_mkProd_or_LetIn eqn type_ctxt 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
       [
@@ -1001,7 +996,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
 	     [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
-	      observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (EConstr.mkVar rec_id)));
+	      observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
 	      (Proofview.V82.of_tactic intros_reflexivity)] g
 	)
       ]
@@ -1014,7 +1009,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
     (mk_equation_id f_id)
     (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem))
     evd
-  lemma_type
+  (EConstr.Unsafe.to_constr lemma_type)
   (Lemmas.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
   Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); 
@@ -1026,10 +1021,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*)
@@ -1038,7 +1033,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
@@ -1054,8 +1049,9 @@ 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 (EConstr.of_constr res) in 
+      let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
       res
   in
   let nb_intro_to_do = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in
@@ -1066,7 +1062,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	  let just_introduced = nLastDecls nb_intro_to_do g' in
           let open Context.Named.Declaration in
 	  let just_introduced_id = List.map get_id just_introduced in
-	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr equation_lemma)))
+	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma))
 		  (revert just_introduced_id) g'
       )
       g
@@ -1103,15 +1099,15 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
     let get_body const =
       match Global.body_of_constant const with
 	| Some body ->
-	     EConstr.Unsafe.to_constr (Tacred.cbv_norm_flags
+	     Tacred.cbv_norm_flags
 	       (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	       (Global.env ())
 	       (Evd.empty)
-	       (EConstr.of_constr 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 =
@@ -1146,35 +1142,35 @@ 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 ->
-		   EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
-		     (EConstr.of_constr (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
-			      List.rev_map var_of_decl princ_params))))
+		   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))
 		)
 		bodies
 	    in
 	    let info_array =
 	      Array.mapi
 		(fun i types ->
-		   let types = Term.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
 		   }
@@ -1186,7 +1182,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
@@ -1196,20 +1192,20 @@ 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 =
-		       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty (EConstr.of_constr (
-			 applist(body,List.rev_map var_of_decl full_params))))
+		       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)) ->
-			       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
-				 (EConstr.of_constr (
+			       Reductionops.nf_betaiota (project g)
+				 (
 				   (applist
 				      (substl
 					 (List.rev
 					    (Array.to_list all_funs_with_full_params))
 					 bs.(num),
 				       List.rev_map var_of_decl princ_params))
-				 ))),num
+				 ),num
 			 | _ -> error "Not a mutual block"
 		   in
 		   let info =
@@ -1238,7 +1234,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	| _, this_fix_info::others_infos ->
 	    let other_fix_infos =
 	      List.map
-		(fun fi -> fi.name,fi.idx + 1 ,EConstr.of_constr fi.types)
+		(fun fi -> fi.name,fi.idx + 1 ,fi.types)
 		(pre_info@others_infos)
 	    in
 	    if List.is_empty other_fix_infos
@@ -1262,11 +1258,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) (EConstr.of_constr (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
@@ -1285,8 +1281,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-		       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
-			 (EConstr.of_constr (applist(fix_body,List.rev_map mkVar args_id))));
+		       Reductionops.nf_betaiota (project g)
+			 (applist(fix_body,List.rev_map mkVar args_id));
 		     eq_hyps = []
 		   }
 		 in
@@ -1345,15 +1341,15 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-		       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
-			 (EConstr.of_constr (applist(fbody_with_full_params,
+		       Reductionops.nf_betaiota Evd.empty
+			 (applist(fbody_with_full_params,
 				  (List.rev_map var_of_decl princ_params)@
 				    (List.rev_map mkVar args_id)
-				 ))));
+				 ));
 		     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 =
@@ -1431,18 +1427,18 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 
 let backtrack_eqs_until_hrec hrec eqs : tactic =
   fun gls ->
-    let eqs = List.map EConstr.mkVar eqs in
+    let eqs = List.map mkVar eqs in
     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 (EConstr.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) (EConstr.of_constr (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) (EConstr.of_constr (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
@@ -1459,7 +1455,7 @@ let rec rewrite_eqs_in_eqs eqs =
 		  observe_tac
 		    (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id))
 		    (tclTRY (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences
-			       true (* dep proofs also: *) true id (EConstr.mkVar eq) false)))
+			       true (* dep proofs also: *) true id (mkVar eq) false)))
 		    gl
 	       )
 	       eqs
@@ -1473,11 +1469,11 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 	 backtrack_eqs_until_hrec hrec eqs;
 	 (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
 	 (tclTHENS  (* We must have exactly ONE subgoal !*)
-	    (Proofview.V82.of_tactic (apply (EConstr.mkVar hrec)))
+	    (Proofview.V82.of_tactic (apply (mkVar hrec)))
 	    [ tclTHENSEQ
 		[
 		  (Proofview.V82.of_tactic (keep (tcc_hyps@eqs)));
-		  (Proofview.V82.of_tactic (apply (EConstr.of_constr (Lazy.force acc_inv))));
+		  (Proofview.V82.of_tactic (apply (Lazy.force acc_inv)));
 		  (fun g ->
 		     if is_mes
 		     then
@@ -1493,7 +1489,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 			    tclCOMPLETE(
 				    Eauto.eauto_with_bases
 				      (true,5)
-				      [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (EConstr.of_constr (Lazy.force refl_equal)) sigma}]
+				      [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
 				      [Hints.Hint_db.empty empty_transparent_state false]
 				  )
 			   )
@@ -1506,20 +1502,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
@@ -1584,7 +1580,7 @@ let prove_principle_for_gen
     Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
   in
   let revert l =
-    tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map EConstr.mkVar l))) (Proofview.V82.of_tactic (clear l))
+    tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
   in
   let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
   let prove_rec_arg_acc g =
@@ -1592,12 +1588,12 @@ let prove_principle_for_gen
 	 (tclCOMPLETE
 	    (tclTHEN
 	       (Proofview.V82.of_tactic (assert_by (Name wf_thm_id)
-		  (EConstr.of_constr (mkApp (delayed_force well_founded,[|input_type;relation|])))
+		  (mkApp (delayed_force well_founded,[|input_type;relation|]))
 		  (Proofview.V82.tactic (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))))
 	       (
 		 (* observe_tac  *)
 (* 		   "apply wf_thm"  *)
-		 Proofview.V82.of_tactic (Tactics.Simple.apply (EConstr.of_constr (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))))
+		 Proofview.V82.of_tactic (Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|])))
 	       )
 	    )
 	 )
@@ -1632,7 +1628,7 @@ let prove_principle_for_gen
 	[
 	  Proofview.V82.of_tactic (generalize [lemma]);
 	  Proofview.V82.of_tactic (Simple.intro hid);
-	  Proofview.V82.of_tactic (Elim.h_decompose_and (EConstr.mkVar hid));
+	  Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
 	  (fun g ->
 	     let new_hyps = pf_ids_of_hyps g in
 	     tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps));
@@ -1656,7 +1652,7 @@ let prove_principle_for_gen
 	);
       (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
 	 (Name acc_rec_arg_id)
- 	 (EConstr.of_constr (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])))
+ 	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
 	 (Proofview.V82.tactic prove_rec_arg_acc)
       );
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
@@ -1665,10 +1661,10 @@ let prove_principle_for_gen
       (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
-      Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_ref)));
+      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') (EConstr.of_constr (pf_concl gl')) in
 	   Array.last args
 	 in
 	 let body_info rec_hyps =
@@ -1711,7 +1707,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 =
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 34ce66967..769d726d7 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -4,7 +4,7 @@ open Term
 val prove_princ_for_struct :
   Evd.evar_map ref ->
   bool ->
-  int -> constant array -> constr array -> int -> Tacmach.tactic
+  int -> constant array -> EConstr.constr array -> int -> Tacmach.tactic
 
 
 val prove_principle_for_gen :
@@ -12,8 +12,8 @@ val prove_principle_for_gen :
   constr option ref -> (* a pointer to the obligation proofs lemma *)
   bool -> (* is that function uses measure *)
   int -> (* the number of recursive argument *)
-  types -> (* the type of the recursive argument *)
-  constr -> (* the wf relation used to prove the function *)
+  EConstr.types -> (* the type of the recursive argument *)
+  EConstr.constr -> (* the wf relation used to prove the function *)
   Tacmach.tactic
 
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8683f68c6..d964002f9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -63,7 +63,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       else args
     in
     Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl),
-                                          compose_prod real_args (mkSort new_sort))
+                                          Term.compose_prod real_args (mkSort new_sort))
   in
   let new_predicates =
     List.map_i
@@ -254,7 +254,7 @@ let change_property_sort evd toSort princ princName =
      let args,ty = decompose_prod (get_type decl) in
      let s = destSort ty in
        Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty);
-       compose_prod args (mkSort toSort)
+       Term.compose_prod args (mkSort toSort)
     )
   in
   let evd,princName_as_constr =
@@ -298,7 +298,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
       hook
   ;
     (*       let _tim1 = System.get_time ()  in *)
-      ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map mkConstU funs) mutr_nparams)));
+      ignore (Pfedit.by  (Proofview.V82.tactic (proof_tac (Array.map EConstr.mkConstU funs) mutr_nparams)));
     (*       let _tim2 =  System.get_time ()  in *)
     (* 	begin *)
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 3fa2644ca..45ad332fc 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -27,7 +27,7 @@ val generate_functional_principle :
   (* The tactic to use to make the proof w.r
      the number of params
   *)
-  (constr array -> int -> Tacmach.tactic) ->
+  (EConstr.constr array -> int -> Tacmach.tactic) ->
   unit
 
 val compute_new_princ_type_from_rel : constr array -> sorts array ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 560242bf2..27a892ca7 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -98,7 +98,6 @@ ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
 END
 
 let functional_induction b c x pat =
-  let x = Option.map (Miscops.map_with_bindings EConstr.Unsafe.to_constr) x in
   Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))
 
 
@@ -110,7 +109,6 @@ TACTIC EXTEND newfunind
 	 | [c] -> c
 	 | c::cl -> EConstr.applist(c,cl)
        in
-       let c = EConstr.Unsafe.to_constr c in
        Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ]
 END
 (***** debug only ***)
@@ -122,7 +120,6 @@ TACTIC EXTEND snewfunind
 	 | [c] -> c
 	 | c::cl -> EConstr.applist(c,cl)
        in
-       let c = EConstr.Unsafe.to_constr c in
        Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ]
 END
 
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0725bb11c..fc5a287ae 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -952,7 +952,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
-		    let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in
+		    let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
 		    let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
 		    let ind,args' = Inductive.find_inductive env ty' in
 		    let mib,_ = Global.lookup_inductive (fst ind) in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 1b899c152..e22fed391 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -2,6 +2,7 @@ open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Pp
 open Indfun_common
 open Libnames
@@ -18,8 +19,8 @@ let is_rec_info sigma scheme_info =
   let test_branche min acc decl =
     acc || (
       let new_branche =
-	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (RelDecl.get_type decl))) in
-      let free_rels_in_br = Termops.free_rels sigma (EConstr.of_constr new_branche) in
+	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (EConstr.of_constr (RelDecl.get_type decl)))) in
+      let free_rels_in_br = Termops.free_rels sigma new_branche in
       let max = min + scheme_info.Tactics.npredicates in
       Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br
     )
@@ -32,20 +33,21 @@ let choose_dest_or_ind scheme_info args =
 
 let functional_induction with_clean c princl pat =
   let res =
-    let f,args = decompose_app c in
     fun g ->
+    let sigma = Tacmach.project g in
+    let f,args = decompose_app sigma c in
     let princ,bindings, princ_type,g' =
       match princl with
       | None -> (* No principle is given let's find the good one *)
 	 begin
-	   match kind_of_term f with
+	   match EConstr.kind sigma f with
 	   | Const (c',u) ->
 	      let princ_option =
 		let finfo = (* we first try to find out a graph on f *)
 		  try find_Function_infos c'
 		  with Not_found ->
 		    user_err  (str "Cannot find induction information on "++
-				       Printer.pr_lconstr (mkConst c') )
+				       Printer.pr_leconstr (mkConst c') )
 		in
 		match Tacticals.elimination_sort_of_goal g with
 		| InProp -> finfo.prop_lemma
@@ -73,15 +75,16 @@ let functional_induction with_clean c princl pat =
 		    (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
 		  with Not_found -> (* This one is neither defined ! *)
 		    user_err  (str "Cannot find induction principle for "
-				     ++Printer.pr_lconstr (mkConst c') )
+				     ++Printer.pr_leconstr (mkConst c') )
 	      in
-	      (princ,NoBindings, Tacmach.pf_unsafe_type_of g' (EConstr.of_constr princ),g')
+	      let princ = EConstr.of_constr princ in
+	      (princ,NoBindings,EConstr.of_constr (Tacmach.pf_unsafe_type_of g' princ),g')
 	   | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
 	 end
       | Some ((princ,binding)) ->
-	 princ,binding,Tacmach.pf_unsafe_type_of g (EConstr.of_constr princ),g
+	 princ,binding,EConstr.of_constr (Tacmach.pf_unsafe_type_of g princ),g
     in
-    let princ_type = EConstr.of_constr princ_type in
+    let sigma = Tacmach.project g' in
     let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in
     let args_as_induction_constr =
       let c_list =
@@ -90,15 +93,13 @@ let functional_induction with_clean c princl pat =
       in
       let encoded_pat_as_patlist =
         List.make (List.length args + List.length c_list - 1) None @ [pat] in
-      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((EConstr.of_constr c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
+      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
         (args@c_list) encoded_pat_as_patlist
     in
-    let princ = EConstr.of_constr princ in
-    let bindings = Miscops.map_bindings EConstr.of_constr bindings in
     let princ' = Some (princ,bindings) in
     let princ_vars =
       List.fold_right
-	(fun a acc -> try Id.Set.add (destVar a) acc with DestKO -> acc)
+	(fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc)
 	args
 	Id.Set.empty
     in
@@ -247,7 +248,8 @@ let derive_inversion fix_names =
 	 let evd,c =
 	   Evd.fresh_global
 	     (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in 
-	 evd, destConst c::l
+        let c = EConstr.of_constr c in
+	 evd, destConst evd c::l
 	)
 	fix_names
 	(evd',[])
@@ -267,7 +269,8 @@ let derive_inversion fix_names =
 	       (Global.env ()) evd
 	       (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id)))
 	   in 
-	   evd,(fst (destInd id))::l
+	   let id = EConstr.of_constr id in
+	   evd,(fst (destInd evd id))::l
 	  )
 	  fix_names
 	  (evd',[])
@@ -334,7 +337,7 @@ let error_error names e =
 
 let generate_principle (evd:Evd.evar_map ref) pconstants on_error
     is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs  interactive_proof
-    (continue_proof : int -> Names.constant array -> Term.constr array -> int ->
+    (continue_proof : int -> Names.constant array -> EConstr.constr array -> int ->
       Tacmach.tactic) : unit =
   let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
@@ -408,7 +411,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
-	    evd,((destConst c)::l)
+            let c = EConstr.of_constr c in
+	    evd,((destConst evd c)::l)
 	   )
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
@@ -422,7 +426,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
-	    evd,((destConst c)::l)
+            let c = EConstr.of_constr c in
+	    evd,((destConst evd c)::l)
 	   )
 	   (Evd.from_env (Global.env ()),[])
 	   fixpoint_exprl
@@ -432,7 +437,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
-    (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic =
+    (_: int) (_:Names.constant array) (_:EConstr.constr array) (_:int) : Tacmach.tactic =
   Functional_principles_proofs.prove_principle_for_gen
     (f_ref,functional_ref,eq_ref)
     tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
@@ -840,7 +845,7 @@ let make_graph (f_ref:global_reference) =
       | ConstRef c ->
 	  begin try c,Global.lookup_constant c
 	  with Not_found ->
-	    raise (UserError (None,str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
+	    raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) )
 	  end
       | _ -> raise (UserError (None, str "Not a function reference") )
   in
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 1c27bdfac..ba89fe4a7 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -12,8 +12,8 @@ val do_generate_principle :
 
 val functional_induction :  
   bool ->
-  Term.constr ->
-  (Term.constr * Term.constr bindings) option ->
+  EConstr.constr ->
+  (EConstr.constr * EConstr.constr bindings) option ->
   Tacexpr.or_and_intro_pattern option ->
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 08b40a1f7..2889d8d03 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -130,8 +130,8 @@ let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
   Nametab.locate (make_qualid dp (Id.of_string s))
 
-let eq = lazy(coq_constant "eq")
-let refl_equal = lazy(coq_constant "eq_refl")
+let eq = lazy(EConstr.of_constr (coq_constant "eq"))
+let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
 
 (*****************************************************************)
 (* Copy of the standart save mechanism but without the much too  *)
@@ -475,13 +475,13 @@ exception ToShow of exn
 let jmeq () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
-    Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq"
+    EConstr.of_constr (Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq")
   with e when CErrors.noncritical e -> raise (ToShow e)
 
 let jmeq_refl () =
   try
     Coqlib.check_required_library Coqlib.jmeq_module_name;
-    Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl"
+    EConstr.of_constr (Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl")
   with e when CErrors.noncritical e -> raise (ToShow e)
 
 let h_intros l =
@@ -489,10 +489,10 @@ let h_intros l =
 
 let h_id = Id.of_string "h"
 let hrec_id = Id.of_string "hrec"
-let well_founded = function () -> (coq_constant "well_founded")
-let acc_rel = function () -> (coq_constant "Acc")
-let acc_inv_id = function () -> (coq_constant "Acc_inv")
-let well_founded_ltof = function () ->  (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
+let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded")
+let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
+let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
+let well_founded_ltof = function () ->  EConstr.of_constr (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
 
 let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
@@ -501,9 +501,45 @@ let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (G
     | VarRef id -> EvalVarRef id
     | _ -> assert false;;
 
-let list_rewrite (rev:bool) (eqs: (constr*bool) list) =
-  let eqs = List.map (Util.on_fst EConstr.of_constr) eqs in
+let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
   tclREPEAT
     (List.fold_right
        (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i)
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
+
+let decompose_lam_n sigma n =
+  let open EConstr in
+  if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive";
+  let rec lamdec_rec l n c =
+    if Int.equal n 0 then l,c
+    else match EConstr.kind sigma c with
+      | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
+      | Cast (c,_,_)     -> lamdec_rec l n c
+      | _ -> CErrors.error "decompose_lam_n: not enough abstractions"
+  in
+  lamdec_rec [] n
+
+let lamn n env b =
+  let open EConstr in
+  let rec lamrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> lamrec (n-1,  l, mkLambda (v,t,b))
+    | _ -> assert false
+  in
+  lamrec (n,env,b)
+
+(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *)
+let compose_lam l b = lamn (List.length l) l b
+
+(* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *)
+let prodn n env b =
+  let open EConstr in
+  let rec prodrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> prodrec (n-1,  l, mkProd (v,t,b))
+    | _ -> assert false
+  in
+  prodrec (n,env,b)
+
+(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
+let compose_prod l b = prodn (List.length l) l b
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index e5c756f56..5836d6519 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -40,11 +40,11 @@ val chop_rprod_n : int -> Glob_term.glob_constr ->
   (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
 
 val def_of_const : Term.constr -> Term.constr
-val eq : Term.constr Lazy.t
-val refl_equal : Term.constr Lazy.t
+val eq : EConstr.constr Lazy.t
+val refl_equal : EConstr.constr Lazy.t
 val const_of_id: Id.t ->  Globnames.global_reference(* constantyes *)
-val jmeq : unit -> Term.constr
-val jmeq_refl : unit -> Term.constr
+val jmeq : unit -> EConstr.constr
+val jmeq_refl : unit -> EConstr.constr
 
 val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Lemmas.declaration_hook CEphemeron.key -> unit
@@ -107,10 +107,15 @@ val is_strict_tcc : unit -> bool
 val h_intros: Names.Id.t list -> Proof_type.tactic
 val h_id :  Names.Id.t
 val hrec_id :  Names.Id.t
-val acc_inv_id :  Term.constr Util.delayed
+val acc_inv_id :  EConstr.constr Util.delayed
 val ltof_ref : Globnames.global_reference Util.delayed
-val well_founded_ltof : Term.constr Util.delayed
-val acc_rel : Term.constr Util.delayed
-val well_founded : Term.constr Util.delayed
+val well_founded_ltof : EConstr.constr Util.delayed
+val acc_rel : EConstr.constr Util.delayed
+val well_founded : EConstr.constr Util.delayed
 val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
-val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic
+val list_rewrite : bool -> (EConstr.constr*bool) list -> Proof_type.tactic
+
+val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
+  (Names.Name.t * EConstr.t) list * EConstr.t
+val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
+val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 27528c2dc..be82010d9 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -12,6 +12,7 @@ open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Vars
 open Pp
 open Globnames
@@ -25,6 +26,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)
+
 (* Some pretty printing function for debugging purpose *)
 
 let pr_binding prc  =
@@ -108,11 +115,11 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
 let make_eq () =
   try
-    Universes.constr_of_global (Coqlib.build_coq_eq ())
+    EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
   with _ -> assert false 
 let make_eq_refl () =
   try
-    Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
+    EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ()))
   with _ -> assert false
 
 	  
@@ -131,16 +138,16 @@ let make_eq_refl () =
 let generate_type evd g_to_f f graph i =
   (*i we deduce the number of arguments of the function and its returned type from the graph i*)
   let evd',graph =
-    Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd graph)))
+    Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd !evd graph)))
   in
+  let graph = EConstr.of_constr graph in
   evd:=evd';
-  let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in
-  let graph_arity = EConstr.Unsafe.to_constr graph_arity in
-  let ctxt,_ = decompose_prod_assum graph_arity in
+  let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+  let ctxt,_ = decompose_prod_assum !evd graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
       | [] | [_] -> anomaly (Pp.str "Not a valid context")
-      | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl
+      | decl :: fun_ctxt -> fun_ctxt, EConstr.of_constr (RelDecl.get_type decl)
   in
   let rec args_from_decl i accu = function
   | [] -> accu
@@ -180,12 +187,12 @@ let generate_type evd g_to_f f graph i =
     \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,  \]
     i*)
   let pre_ctxt =
-    LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt
+    local_assum (Name res_id, lift 1 res_type) :: local_def (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt
   in
   (*i and we can return the solution depending on which lemma type we are defining i*)
   if g_to_f
-  then LocalAssum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
-  else LocalAssum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
+  then local_assum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
+  else local_assum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
 
 
 (*
@@ -194,7 +201,7 @@ let generate_type evd g_to_f f graph i =
    WARNING: while convertible, [type_of body] and [type] can be non equal
 *)
 let find_induction_principle evd f =
-  let f_as_constant,u =  match kind_of_term f with
+  let f_as_constant,u =  match EConstr.kind !evd f with
     | Const c' -> c'
     | _ -> error "Must be used with a function"
   in
@@ -203,8 +210,8 @@ let find_induction_principle evd f =
     | None -> raise Not_found
     | Some rect_lemma ->
        let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
-       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in
-       let typ = EConstr.Unsafe.to_constr typ in
+       let rect_lemma = EConstr.of_constr rect_lemma in
+       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
        evd:=evd';
        rect_lemma,typ
 
@@ -248,12 +255,12 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
        \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun  fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
     *)
     (* we the get the definition of the graphs block *)
-    let graph_ind,u = destInd graphs_constr.(i) in
+    let graph_ind,u = destInd evd graphs_constr.(i) in
     let kn = fst graph_ind in
     let mib,_ = Global.lookup_inductive graph_ind in
     (* and the principle to use in this lemma in $\zeta$ normal form *)
     let f_principle,princ_type = schemes.(i) in
-    let princ_type =  nf_zeta (EConstr.of_constr princ_type) in
+    let princ_type =  nf_zeta princ_type in
     let princ_infos = Tactics.compute_elim_sig evd princ_type in
     (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
@@ -273,13 +280,13 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	(fun decl ->
 	   List.map
 	     (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
-	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (RelDecl.get_type decl)))))
+	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (EConstr.of_constr (RelDecl.get_type decl))))))
 	)
 	branches
     in
     (* before building the full intro pattern for the principle *)
     let eq_ind = make_eq () in
-    let eq_construct = mkConstructUi (destInd eq_ind, 1) in
+    let eq_construct = mkConstructUi (destInd evd eq_ind, 1) in
     (* The next to referencies will be used to find out which constructor to apply in each branch *)
     let ind_number = ref 0
     and min_constr_number = ref 0 in
@@ -307,18 +314,20 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let constructor_args g =
 	List.fold_right 
 	  (fun hid acc ->
-	     let type_of_hid = pf_unsafe_type_of g (EConstr.mkVar hid) in
-	     match kind_of_term type_of_hid with
+	     let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
+	     let type_of_hid = EConstr.of_constr type_of_hid in
+	     let sigma = project g in
+	     match EConstr.kind sigma type_of_hid with
 	       | Prod(_,_,t') ->
 		   begin
-		     match kind_of_term t' with
+		     match EConstr.kind sigma t' with
 		       | Prod(_,t'',t''') ->
 			   begin
-			     match kind_of_term t'',kind_of_term t''' with
+			     match EConstr.kind sigma t'',EConstr.kind sigma t''' with
 			       | App(eq,args), App(graph',_)
 				   when
-				     (Term.eq_constr eq eq_ind) &&
-				       Array.exists  (Constr.eq_constr_nounivs graph') graphs_constr ->
+				     (EConstr.eq_constr sigma eq eq_ind) &&
+				       Array.exists  (EConstr.eq_constr_nounivs sigma graph') graphs_constr ->
 				   (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
 				    ::acc)
 			       | _ -> mkVar hid ::  acc
@@ -386,10 +395,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    (* introducing the the result of the graph and the equality hypothesis *)
 	    observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
 	    (* replacing [res] with its value *)
-	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar hres)));
+	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g ->
-				 Proofview.V82.of_tactic (exact_check (EConstr.of_constr (app_constructor g))) g)  
+				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
 	  ]
       )
 	g
@@ -401,8 +410,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	   match ctxt with
 	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
 	     | hres::res::decl::ctxt ->
-		let res = Term.it_mkLambda_or_LetIn
-			    (Term.it_mkProd_or_LetIn concl [hres;res])
+		let res = EConstr.it_mkLambda_or_LetIn
+			    (EConstr.it_mkProd_or_LetIn concl [hres;res])
 			    (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt)
 		in
 		res
@@ -430,7 +439,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
-	     (EConstr.Unsafe.to_constr (nf_zeta (EConstr.of_constr p)))::bindings,id::avoid)
+	     (nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
@@ -442,7 +451,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
 	  (Name principle_id)
 	  princ_type
-	  (exact_check (EConstr.of_constr f_principle))));
+	  (exact_check f_principle)));
 	observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names);
 	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
 	observe_tac "idtac" tclIDTAC;
@@ -451,8 +460,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	     "functional_induction" (
 	       (fun gl ->
 		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
-		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl (EConstr.of_constr term) in
-		Proofview.V82.of_tactic (apply (EConstr.of_constr term)) gl')
+		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl term in
+		Proofview.V82.of_tactic (apply term) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
       ]
@@ -469,7 +478,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | LocalAssum (id,t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [EConstr.mkVar id])) (thin [id])
+	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -493,44 +502,45 @@ let  rec intros_with_rewrite g =
 and intros_with_rewrite_aux : tactic =
   fun g ->
     let eq_ind = make_eq () in
-    match kind_of_term (pf_concl g) with
+    let sigma = project g in
+    match EConstr.kind sigma (EConstr.of_constr (pf_concl g)) with
 	  | Prod(_,t,t') ->
 	      begin
-		match kind_of_term t with
-		  | App(eq,args) when (Term.eq_constr eq eq_ind)  ->
- 		      if Reductionops.is_conv (pf_env g) (project g) (EConstr.of_constr args.(1)) (EConstr.of_constr args.(2))
+		match EConstr.kind sigma t with
+		  | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind)  ->
+ 		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
-		      else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) 
+		      else if isVar sigma args.(1) && (Environ.evaluable_named (destVar sigma args.(1)) (pf_env g)) 
 		      then tclTHENSEQ[
-			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]);
-			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )))
+			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))]);
+			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))] ((destVar sigma args.(1)),Locus.InHyp) )))
 			  (pf_ids_of_hyps g);
 			intros_with_rewrite
 		      ] g
-		      else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g)) 
+		      else if isVar sigma args.(2) && (Environ.evaluable_named (destVar sigma args.(2)) (pf_env g)) 
 		      then tclTHENSEQ[
-			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]);
-			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )))
+			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))]);
+			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))] ((destVar sigma args.(2)),Locus.InHyp) )))
 			  (pf_ids_of_hyps g);
 			intros_with_rewrite
 		      ] g
-		      else if isVar args.(1)
+		      else if isVar sigma args.(1)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
-				     generalize_dependent_of (destVar args.(1)) id;
-				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id)));
+				     generalize_dependent_of (destVar sigma args.(1)) id;
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
-		      else if isVar args.(2) 
+		      else if isVar sigma args.(2) 
 		      then 
 			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
-				     generalize_dependent_of (destVar args.(2)) id;
-				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar id)));
+				     generalize_dependent_of (destVar sigma args.(2)) id;
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
@@ -539,15 +549,15 @@ and intros_with_rewrite_aux : tactic =
 			  let id = pf_get_new_id (Id.of_string "y") g  in
 			  tclTHENSEQ[
 			    Proofview.V82.of_tactic (Simple.intro id);
-			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id)));
+			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 			    intros_with_rewrite
 			  ] g
 			end
-		  | Ind _ when Term.eq_constr t (Coqlib.build_coq_False ()) ->
+		  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Coqlib.build_coq_False ())) ->
 		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
-			Proofview.V82.of_tactic (simplest_case (EConstr.of_constr v));
+			Proofview.V82.of_tactic (simplest_case v);
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
@@ -581,10 +591,10 @@ and intros_with_rewrite_aux : tactic =
 let rec reflexivity_with_destruct_cases g =
   let destruct_case () =
     try
-      match kind_of_term (snd (destApp (pf_concl g))).(2) with
+      match EConstr.kind (project g) (snd (destApp (project g) (EConstr.of_constr (pf_concl g)))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
-	      Proofview.V82.of_tactic (simplest_case (EConstr.of_constr v));
+	      Proofview.V82.of_tactic (simplest_case v);
 	      Proofview.V82.of_tactic intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
@@ -598,11 +608,11 @@ let rec reflexivity_with_destruct_cases g =
 	 match sc with
 	     None -> tclIDTAC g
 	   | Some id ->
-	       match kind_of_term  (pf_unsafe_type_of g (EConstr.mkVar id)) with
-		 | App(eq,[|_;t1;t2|]) when Term.eq_constr eq eq_ind ->
-		     if Equality.discriminable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
+	       match EConstr.kind (project g) (EConstr.of_constr (pf_unsafe_type_of g (mkVar id))) with
+		 | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
+		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
-		     else if Equality.injectable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
+		     else if Equality.injectable (pf_env g) (project g) t1 t2
 		     then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
@@ -657,7 +667,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     *)
     let lemmas =
       Array.map
-	(fun (_,(ctxt,concl)) -> nf_zeta (EConstr.of_constr (Termops.it_mkLambda_or_LetIn concl ctxt)))
+	(fun (_,(ctxt,concl)) -> nf_zeta (EConstr.it_mkLambda_or_LetIn concl ctxt))
 	lemmas_types_infos
     in
     (* We get the constant and the principle corresponding to this lemma *)
@@ -698,7 +708,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let rewrite_tac j ids : tactic =
       let graph_def = graphs.(j) in
       let infos =
-        try find_Function_infos (fst (destConst funcs.(j)))
+        try find_Function_infos (fst (destConst (project g) funcs.(j)))
         with Not_found ->  error "No graph found"
       in
       if infos.is_general
@@ -710,7 +720,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	in
 	tclTHENSEQ[
 	  tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
-	  Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_lemma)));
+	  Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
 	  (* Don't forget to $\zeta$ normlize the term since the principles
              have been $\zeta$-normalized *)
 	  Proofview.V82.of_tactic (reduce
@@ -720,11 +730,11 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	       })
 	    Locusops.onConcl)
 	  ;
-	  Proofview.V82.of_tactic (generalize (List.map EConstr.mkVar ids));
+	  Proofview.V82.of_tactic (generalize (List.map mkVar ids));
 	  thin ids
 	]
       else
-        Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))])
+        Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst (project g) f)))])
     in
     (* The proof of each branche itself *)
     let ind_number = ref 0 in
@@ -795,11 +805,10 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 in
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
-	 let type_of_lemma = Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-	 let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in 
-	   let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
-	   let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
-	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
+	 let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
+	 let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in 
+	   let type_of_lemma = nf_zeta type_of_lemma in
+	   observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
 	)
 	funs_constr
@@ -818,7 +827,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	  Array.of_list
 	    (List.map
 	       (fun entry ->
-		  (fst (fst(Future.force entry.Entries.const_entry_body)), Option.get entry.Entries.const_entry_type )
+		  (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type ))
 	       )
 	       (make_scheme evd (Array.map_to_list (fun const -> const,GType []) funs))
 	    )
@@ -839,7 +848,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	   lem_id
 	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem)))
            !evd
-	   typ
+	   (EConstr.Unsafe.to_constr typ)
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
@@ -849,7 +858,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
 	 let _,lem_cst_constr = Evd.fresh_global
 				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
-	 let (lem_cst,_) = destConst lem_cst_constr in
+        let lem_cst_constr = EConstr.of_constr lem_cst_constr in
+	 let (lem_cst,_) = destConst !evd lem_cst_constr in
 	 update_Function {finfo with correctness_lemma = Some lem_cst};
 
       )
@@ -863,18 +873,17 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma =
-	   Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
+	   EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
 	 in
-	 let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
-	 let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
-	 observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
+	 let type_of_lemma = nf_zeta type_of_lemma in
+	 observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma);
 	 type_of_lemma,type_info
 	)
 	funs_constr
 	graphs_constr
     in
 
-    let (kn,_) as graph_ind,u  = (destInd graphs_constr.(0)) in
+    let (kn,_) as graph_ind,u  = (destInd !evd graphs_constr.(0)) in
     let mib,mip = Global.lookup_inductive graph_ind in
     let sigma, scheme = 
 	(Indrec.build_mutual_induction_scheme (Global.env ()) !evd
@@ -901,7 +910,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
-	 (fst lemmas_types_infos.(i))
+	 (EConstr.Unsafe.to_constr (fst lemmas_types_infos.(i)))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
@@ -910,7 +919,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let finfo = find_Function_infos (fst f_as_constant) in
 	 let _,lem_cst_constr = Evd.fresh_global
 				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
-	 let (lem_cst,_) = destConst lem_cst_constr in
+         let lem_cst_constr = EConstr.of_constr lem_cst_constr in
+	 let (lem_cst,_) = destConst !evd lem_cst_constr in
 	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs)
@@ -925,10 +935,12 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
    if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
 *)
 let revert_graph kn post_tac hid g =
-    let typ = pf_unsafe_type_of g (EConstr.mkVar hid) in
-    match kind_of_term typ with
-      | App(i,args) when isInd i ->
-	  let ((kn',num) as ind'),u = destInd i in
+    let sigma = project g in
+    let typ = pf_unsafe_type_of g (mkVar hid) in
+    let typ = EConstr.of_constr typ in
+    match EConstr.kind sigma typ with
+      | App(i,args) when isInd sigma i ->
+	  let ((kn',num) as ind'),u = destInd sigma i in
 	  if MutInd.equal kn kn'
 	  then (* We have generated a graph hypothesis so that we must change it if we can *)
 	    let info =
@@ -945,7 +957,7 @@ let revert_graph kn post_tac hid g =
 		  let f_args,res = Array.chop (Array.length args - 1) args in
 		  tclTHENSEQ
 		    [
-		      Proofview.V82.of_tactic (generalize [EConstr.of_constr (applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid]))]);
+		      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
 		      thin [hid];
 		      Proofview.V82.of_tactic (Simple.intro hid);
 		      post_tac hid
@@ -976,20 +988,22 @@ let revert_graph kn post_tac hid g =
 let functional_inversion kn hid fconst f_correct : tactic =
   fun g ->
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
-    let type_of_h = pf_unsafe_type_of g (EConstr.mkVar hid) in
-    match kind_of_term type_of_h with
-      | App(eq,args) when Term.eq_constr eq (make_eq ())  ->
+    let sigma = project g in
+    let type_of_h = pf_unsafe_type_of g (mkVar hid) in
+    let type_of_h = EConstr.of_constr type_of_h in
+    match EConstr.kind sigma type_of_h with
+      | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
-	    match kind_of_term args.(1),kind_of_term args.(2) with
-	      | App(f,f_args),_ when Term.eq_constr f fconst ->
+	    match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with
+	      | App(f,f_args),_ when EConstr.eq_constr sigma f fconst ->
 		  ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2))
-	      |_,App(f,f_args) when Term.eq_constr f fconst ->
+	      |_,App(f,f_args) when EConstr.eq_constr sigma f fconst ->
 		 ((fun hid -> tclIDTAC),f_args,args.(1))
 	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
 	  in
 	  tclTHENSEQ[
 	    pre_tac hid;
-	    Proofview.V82.of_tactic (generalize [EConstr.of_constr (applist(f_correct,(Array.to_list f_args)@[res;mkVar hid]))]);
+	    Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
 	    thin [hid];
 	    Proofview.V82.of_tactic (Simple.intro hid);
 	    Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
@@ -1028,23 +1042,25 @@ let invfun qhyp f g =
        Proofview.V82.of_tactic begin
 	Tactics.try_intros_until
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
-	     let hyp_typ = pf_unsafe_type_of g (EConstr.mkVar hid)  in
-	     match kind_of_term hyp_typ with
-	       | App(eq,args) when Term.eq_constr eq (make_eq ()) ->
+            let sigma = project g in
+	     let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
+	     let hyp_typ = EConstr.of_constr hyp_typ in
+	     match EConstr.kind sigma hyp_typ with
+	       | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
 		   begin
-		     let f1,_ = decompose_app args.(1) in
+		     let f1,_ = decompose_app sigma args.(1) in
 		     try
-		       if not (isConst f1) then failwith "";
-		       let finfos = find_Function_infos (fst (destConst f1)) in
+		       if not (isConst sigma f1) then failwith "";
+		       let finfos = find_Function_infos (fst (destConst sigma f1)) in
 		       let f_correct = mkConst(Option.get finfos.correctness_lemma)
 		       and kn = fst finfos.graph_ind
 		       in
 		       functional_inversion kn hid f1 f_correct g
 		     with | Failure "" | Option.IsNone | Not_found ->
 		       try
-			 let f2,_ = decompose_app args.(2) in
-			 if not (isConst f2) then failwith "";
-			 let finfos = find_Function_infos (fst (destConst f2)) in
+			 let f2,_ = decompose_app sigma args.(2) in
+			 if not (isConst sigma f2) then failwith "";
+			 let finfos = find_Function_infos (fst (destConst sigma f2)) in
 			 let f_correct = mkConst(Option.get finfos.correctness_lemma)
 			 and kn = fst finfos.graph_ind
 			 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 23b308efb..a80a7b5e7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -6,7 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module CVars = Vars
+
 open Term
+open EConstr
 open Vars
 open Namegen
 open Environ
@@ -42,17 +45,22 @@ open Indfun_common
 open Sigma.Notations
 open Context.Rel.Declaration
 
+let local_assum (na, t) =
+  LocalAssum (na, EConstr.Unsafe.to_constr t)
+
+let local_def (na, b, t) =
+  LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
 
 (* Ugly things which should not be here *)
 
 let coq_constant m s =
-  Coqlib.coq_constant "RecursiveDefinition" m s
+  EConstr.of_constr (Coqlib.coq_constant "RecursiveDefinition" m s)
 
 let arith_Nat = ["Arith";"PeanoNat";"Nat"]
 let arith_Lt = ["Arith";"Lt"]
 
 let coq_init_constant s =
-  Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s
+  EConstr.of_constr (Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s)
 
 let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
@@ -76,8 +84,8 @@ let def_of_const t =
       )
      |_ -> assert false
 
-let type_of_const t =
-   match (kind_of_term t) with
+let type_of_const sigma t =
+   match (EConstr.kind sigma t) with
     Const sp -> Typeops.type_of_constant (Global.env()) sp
     |_ -> assert false
 
@@ -98,9 +106,7 @@ let nf_zeta env =
 
 
 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
 
 
 
@@ -116,8 +122,8 @@ let pf_get_new_ids idl g =
     []
 
 let compute_renamed_type gls c =
-  rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
-    (pf_unsafe_type_of gls (EConstr.of_constr c))
+  EConstr.of_constr (rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
+    (pf_unsafe_type_of gls c))
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
 let ano_id = Id.of_string "anonymous"
@@ -147,7 +153,7 @@ let coq_O = function () -> (coq_init_constant "O")
 let coq_S = function () -> (coq_init_constant "S")
 let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
 let max_ref = function () -> (find_reference ["Recdef"] "max")
-let max_constr = function () -> (constr_of_global (delayed_force max_ref))
+let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref))
 let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj"
 
 let f_S t = mkApp(delayed_force coq_S, [|t|]);;
@@ -166,7 +172,8 @@ let simpl_iter clause =
     clause
 
 (* Others ugly things ... *)
-let (value_f:constr list -> global_reference -> constr) =
+let (value_f:Constr.constr list -> global_reference -> Constr.constr) =
+  let open Term in
   fun al fterm ->
     let d0 = Loc.ghost in
     let rev_x_id_l =
@@ -199,7 +206,7 @@ let (value_f:constr list -> global_reference -> constr) =
     let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
     it_mkLambda_or_LetIn body context
 
-let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) =
+let (declare_f : Id.t -> logical_kind -> Constr.constr list -> global_reference -> global_reference) =
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
@@ -286,7 +293,7 @@ let tclUSER tac is_mes l g =
 
 let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
   if is_mes
-  then tclCOMPLETE (fun gl -> Proofview.V82.of_tactic (Simple.apply (EConstr.of_constr (delayed_force well_founded_ltof))) gl)
+  then tclCOMPLETE (fun gl -> Proofview.V82.of_tactic (Simple.apply (delayed_force well_founded_ltof)) gl)
   else (* tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) *) (tclUSER concl_tac is_mes names_to_suppress)
 
 
@@ -301,9 +308,9 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
 (* [check_not_nested forbidden e] checks that [e] does not contains any variable 
    of [forbidden]
 *)
-let check_not_nested forbidden e =
+let check_not_nested sigma forbidden e =
   let rec check_not_nested e =  
-    match kind_of_term e with 
+    match EConstr.kind sigma e with 
       | Rel _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
@@ -327,7 +334,7 @@ let check_not_nested forbidden e =
   try 
     check_not_nested e 
   with UserError(_,p) -> 
-    user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
+    user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr e ++ str " " ++ p)
 
 (* ['a info] contains the local information for traveling *)
 type 'a infos = 
@@ -374,15 +381,17 @@ type journey_info =
 
 	       
 
-let rec add_vars forbidden e = 
-  match kind_of_term e with 
+let add_vars sigma forbidden e = 
+  let rec aux forbidden e =
+  match EConstr.kind sigma e with 
     | Var x -> x::forbidden 
-    | _ -> Term.fold_constr add_vars forbidden e
-
+    | _ -> EConstr.fold sigma aux forbidden e
+  in
+  aux forbidden e
 
 let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = 
   fun g -> 
-    let rev_context,b = decompose_lam_n nb_lam e in 
+    let rev_context,b = decompose_lam_n (project g) nb_lam e in
     let ids = List.fold_left (fun acc (na,_) -> 	
       let pre_id = 
 	match na with 
@@ -402,20 +411,20 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	    Proofview.V82.of_tactic (clear to_intros);
 	    h_intros to_intros;
 	    (fun g' -> 
-	      let ty_teq = pf_unsafe_type_of g' (EConstr.mkVar heq) in
+	      let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
+	      let ty_teq = EConstr.of_constr ty_teq in
 	      let teq_lhs,teq_rhs =
-		let _,args = try destApp ty_teq with DestKO -> assert false in
+		let _,args = try destApp (project g') ty_teq with DestKO -> assert false in
 		args.(1),args.(2)
 	      in
-	      let new_b' = Termops.replace_term (project g') (EConstr.of_constr teq_lhs) (EConstr.of_constr teq_rhs) (EConstr.of_constr new_b) in 
-	      let new_b' = EConstr.Unsafe.to_constr new_b' in
+	      let new_b' = Termops.replace_term (project g') teq_lhs teq_rhs new_b in 
 	      let new_infos = {
 		infos with 
 		  info = new_b';
 		  eqs = heq::infos.eqs;
 		  forbidden_ids = 
 		  if forbid_new_ids 
-		  then add_vars infos.forbidden_ids new_b'
+		  then add_vars (project g') infos.forbidden_ids new_b'
 		  else infos.forbidden_ids
 	      } in 
 	      finalize_tac new_infos g' 
@@ -424,8 +433,9 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	)
       ] g
 
-let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
-  match kind_of_term expr_info.info with 
+let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
+  let sigma = project g in
+  match EConstr.kind sigma expr_info.info with 
     | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint"
     | Proj _ -> error "Function cannot treat projections"
     | LetIn(na,b,t,e) -> 
@@ -434,24 +444,24 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	  jinfo.letiN (na,b,t,e) expr_info continuation_tac
 	in
 	travel jinfo new_continuation_tac 
-	  {expr_info with info = b; is_final=false}
+	  {expr_info with info = b; is_final=false} g
       end
     | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
     | Prod _ -> 
       begin
 	try
-	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
-	  jinfo.otherS () expr_info continuation_tac expr_info
+	  check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
+	  jinfo.otherS () expr_info continuation_tac expr_info g
 	with e when CErrors.noncritical e ->
-	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Lambda(n,t,b) -> 
       begin
 	try
-	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
-	  jinfo.otherS () expr_info continuation_tac expr_info
+	  check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
+	  jinfo.otherS () expr_info continuation_tac expr_info g
 	with e when CErrors.noncritical e ->
-	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Case(ci,t,a,l) -> 
       begin
@@ -462,15 +472,15 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	travel 
 	  jinfo continuation_tac_a 
 	  {expr_info with info = a; is_main_branch = false; 
-	    is_final = false}
+	    is_final = false} g
       end
     | App _ -> 
-      let f,args = decompose_app expr_info.info in 
-      if Term.eq_constr f (expr_info.f_constr) 
-      then jinfo.app_reC (f,args) expr_info continuation_tac expr_info 
+      let f,args = decompose_app sigma expr_info.info in 
+      if EConstr.eq_constr sigma f (expr_info.f_constr) 
+      then jinfo.app_reC (f,args) expr_info continuation_tac expr_info g
       else
       begin
-	match kind_of_term f with 
+	match EConstr.kind sigma f with 
 	  | App _ -> assert false (* f is coming from a decompose_app *)
 	  | Const _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ 
 	  | Sort _ | Prod _ | Var _ -> 
@@ -478,15 +488,15 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	    let new_continuation_tac = 
 	      jinfo.apP (f,args) expr_info continuation_tac in 
 	    travel_args jinfo
-	      expr_info.is_main_branch new_continuation_tac new_infos
-	  | Case _ ->  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
-	  | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_lconstr expr_info.info)
+	      expr_info.is_main_branch new_continuation_tac new_infos g
+	  | Case _ ->  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
+	  | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info)
       end
-    | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t}
+    | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
     | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
       let new_continuation_tac = 
 	jinfo.otherS () expr_info continuation_tac in
-      new_continuation_tac expr_info
+      new_continuation_tac expr_info g
 and travel_args jinfo is_final continuation_tac infos = 
   let (f_args',args) = infos.info in 
   match args with 
@@ -503,36 +513,37 @@ and travel_args jinfo is_final continuation_tac infos =
 	{infos with info=arg;is_final=false} 
 and travel jinfo continuation_tac expr_info = 
   observe_tac 
-    (str jinfo.message ++ Printer.pr_lconstr expr_info.info) 
+    (str jinfo.message ++ Printer.pr_leconstr expr_info.info) 
     (travel_aux jinfo continuation_tac expr_info)
 
 (* Termination proof *) 
 
 let rec prove_lt hyple g = 
+  let sigma = project g in
   begin
     try
-      let (varx,varz) = match decompose_app (pf_concl g) with
-        | _, x::z::_ when isVar x && isVar z -> x, z
+      let (varx,varz) = match decompose_app sigma (EConstr.of_constr (pf_concl g)) with
+        | _, x::z::_ when isVar sigma x && isVar sigma z -> x, z
         | _ -> assert false
       in
       let h =
 	List.find (fun id ->
-          match decompose_app (pf_unsafe_type_of g (EConstr.mkVar id)) with
-            | _, t::_ -> Term.eq_constr t varx
+          match decompose_app sigma (EConstr.of_constr (pf_unsafe_type_of g (mkVar id))) with
+            | _, t::_ -> EConstr.eq_constr sigma t varx
             | _ -> false
 	) hyple
       in
       let y =
-	List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (EConstr.mkVar h))))) in
+	List.hd (List.tl (snd (decompose_app sigma (EConstr.of_constr (pf_unsafe_type_of g (mkVar h)))))) in
       observe_tclTHENLIST (str "prove_lt1")[
-	Proofview.V82.of_tactic (apply (EConstr.of_constr (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))));
+	Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
 	observe_tac (str "prove_lt") (prove_lt hyple)
       ]
     with Not_found -> 
       (
 	(
 	  observe_tclTHENLIST (str "prove_lt2")[
-	    Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force lt_S_n)));
+	    Proofview.V82.of_tactic (apply (delayed_force lt_S_n));
 	    (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption))
 	  ])
       )
@@ -550,15 +561,15 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
       let ids = h'::ids in
       let def = next_ident_away_in_goal def_id ids in
       observe_tclTHENLIST (str "destruct_bounds_aux1")[
-	Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr s_max]));
+	Proofview.V82.of_tactic (split (ImplicitBindings [s_max]));
 	Proofview.V82.of_tactic (intro_then
 	  (fun id -> 
             Proofview.V82.tactic begin
 	    observe_tac (str "destruct_bounds_aux") 
-	      (tclTHENS (Proofview.V82.of_tactic (simplest_case (EConstr.mkVar id)))
+	      (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id)))
 		 [
 		   observe_tclTHENLIST (str "")[Proofview.V82.of_tactic (intro_using h_id);
-			       Proofview.V82.of_tactic (simplest_elim(EConstr.of_constr (mkApp(delayed_force lt_n_O,[|s_max|]))));
+			       Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
 			       Proofview.V82.of_tactic default_full_auto];
 		   observe_tclTHENLIST (str "destruct_bounds_aux2")[
 		     observe_tac (str "clearing k ") (Proofview.V82.of_tactic (clear [id]));
@@ -589,7 +600,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 	  ] g
       | (_,v_bound)::l -> 
       observe_tclTHENLIST (str "destruct_bounds_aux3")[
-	Proofview.V82.of_tactic (simplest_elim (EConstr.mkVar v_bound));
+	Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
 	Proofview.V82.of_tactic (clear [v_bound]);
 	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 
@@ -598,7 +609,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 	       (fun p ->  
 		 observe_tclTHENLIST (str "destruct_bounds_aux4")[
 		   Proofview.V82.of_tactic (simplest_elim 
-		     (EConstr.of_constr (mkApp(delayed_force max_constr, [| bound; mkVar p|]))));
+		     (mkApp(delayed_force max_constr, [| bound; mkVar p|])));
 		   tclDO 3 (Proofview.V82.of_tactic intro);
 		   onNLastHypsId 3 (fun lids -> 
 		     match lids with
@@ -623,7 +634,7 @@ let terminate_app f_and_args expr_info continuation_tac infos =
       observe_tclTHENLIST (str "terminate_app1")[
 	continuation_tac infos;
 	observe_tac (str "first split") 
-	  (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr infos.info])));
+	  (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
 	observe_tac (str "destruct_bounds (1)") (destruct_bounds infos)
       ]
     else continuation_tac infos
@@ -634,17 +645,18 @@ let terminate_others _ expr_info continuation_tac infos =
     observe_tclTHENLIST (str "terminate_others")[
 	    continuation_tac infos;
       observe_tac (str "first split") 
-	(Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr infos.info])));
+	(Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
       observe_tac (str "destruct_bounds") (destruct_bounds infos)
     ]
   else continuation_tac infos
 
-let terminate_letin (na,b,t,e) expr_info continuation_tac info = 
+let terminate_letin (na,b,t,e) expr_info continuation_tac info g =
+  let sigma = project g in
   let new_e = subst1 info.info e in 
   let new_forbidden = 
     let forbid = 
       try 
-	check_not_nested (expr_info.f_id::expr_info.forbidden_ids) b;
+	check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) b;
 	true
       with e when CErrors.noncritical e -> false
     in
@@ -655,7 +667,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
 	| Name id -> id::info.forbidden_ids
     else info.forbidden_ids 
   in
-  continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} 
+  continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g
 
 let pf_type c tac gl = 
   let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
@@ -682,30 +694,31 @@ let mkDestructEq :
       (fun decl ->
         let open Context.Named.Declaration in
         let id = get_id decl in
-        if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) (EConstr.of_constr expr) (EConstr.of_constr (get_type decl)))
+        if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) expr (EConstr.of_constr (get_type decl)))
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
-  let type_of_expr = pf_unsafe_type_of g (EConstr.of_constr expr) in
+  let type_of_expr = pf_unsafe_type_of g expr in
+  let type_of_expr = EConstr.of_constr type_of_expr in
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
            to_revert_constr in
-  let new_hyps = List.map EConstr.of_constr new_hyps in
     pf_typel new_hyps (fun _ ->
     observe_tclTHENLIST (str "mkDestructEq")
      [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
         let changefun patvars = { run = fun sigma ->
-          let redfun = pattern_occs [Locus.AllOccurrencesBut [1], EConstr.of_constr expr] in
+          let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
           let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2)) in
           Sigma (c, sigma, p)
         } in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
-      Proofview.V82.of_tactic (simplest_case (EConstr.of_constr expr))]), to_revert
+      Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
 
 let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
+  let sigma = project g in
   let f_is_present =
     try
-      check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a;
+      check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) a;
       false
     with e when CErrors.noncritical e ->
       true
@@ -719,7 +732,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
   let destruct_tac,rev_to_thin_intro = 
     mkDestructEq [expr_info.rec_arg_id] a' g in 
   let to_thin_intro = List.rev rev_to_thin_intro in 
-  observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_lconstr a') 
+  observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr a') 
     (try
       (tclTHENS
 	 destruct_tac
@@ -728,16 +741,17 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
     with 
       | UserError(Some "Refiner.thensn_tac3",_) 
       | UserError(Some "Refiner.tclFAIL_s",_) ->
-	(observe_tac (str "is computable " ++ Printer.pr_lconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
+	(observe_tac (str "is computable " ++ Printer.pr_leconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
 	))
     g
     
-let terminate_app_rec (f,args) expr_info continuation_tac _ = 
-  List.iter (check_not_nested (expr_info.f_id::expr_info.forbidden_ids))
+let terminate_app_rec (f,args) expr_info continuation_tac _ g =
+  let sigma = project g in
+  List.iter (check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids))
     args;
   begin
     try 
-      let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in
+      let v = List.assoc_f (List.equal (EConstr.eq_constr sigma)) args expr_info.args_assoc in
       let new_infos = {expr_info with info = v} in 
       observe_tclTHENLIST (str "terminate_app_rec")[
 	continuation_tac new_infos;
@@ -745,16 +759,16 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 	then
 	  observe_tclTHENLIST (str "terminate_app_rec1")[ 
 	    observe_tac (str "first split")
-	      (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr new_infos.info])));
+	      (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
 	    observe_tac (str "destruct_bounds (3)")
 	      (destruct_bounds new_infos)
 	  ]
 	else
 	  tclIDTAC			       
-      ]    
+      ] g
     with Not_found -> 
       observe_tac (str "terminate_app_rec not found") (tclTHENS
-	(Proofview.V82.of_tactic (simplest_elim (EConstr.of_constr (mkApp(mkVar expr_info.ih,Array.of_list args)))))
+	(Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args))))
 	[		
 	  observe_tclTHENLIST (str "terminate_app_rec2")[
 	    Proofview.V82.of_tactic (intro_using rec_res_id);
@@ -775,7 +789,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 		       then
 			 observe_tclTHENLIST (str "terminate_app_rec4")[ 
 			   observe_tac (str "first split") 
-			     (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr new_infos.info])));
+			     (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
 			   observe_tac (str "destruct_bounds (2)") 
 			     (destruct_bounds new_infos)
 			 ]
@@ -788,7 +802,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 	  ];
 	  observe_tac (str "proving decreasing") (
 	    tclTHENS (* proof of args < formal args *)
-	      (Proofview.V82.of_tactic (apply (EConstr.of_constr (Lazy.force expr_info.acc_inv))))
+	      (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv)))
 	      [ 
 		observe_tac (str "assumption") (Proofview.V82.of_tactic assumption);
 		observe_tclTHENLIST (str "terminate_app_rec5")
@@ -808,7 +822,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 		      );
 		  ]
 	      ])
-	])
+	]) g
   end
 
 let terminate_info = 
@@ -830,26 +844,28 @@ let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos =
   observe_tac (str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos)
 
 let rec prove_le g = 
+  let sigma = project g in
   let x,z = 
-    let _,args = decompose_app (pf_concl g) in 
+    let _,args = decompose_app sigma (EConstr.of_constr (pf_concl g)) in 
     (List.hd args,List.hd (List.tl args))
   in 
   tclFIRST[
     Proofview.V82.of_tactic assumption;
-    Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_n)));
+    Proofview.V82.of_tactic (apply (delayed_force le_n));
     begin
       try
 	let matching_fun = 
 	  pf_is_matching g
-	    (Pattern.PApp(Pattern.PRef (reference_of_constr (le ())),[|Pattern.PVar (destVar x);Pattern.PMeta None|])) in 
+	    (Pattern.PApp(Pattern.PRef (reference_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in 
 	let (h,t) = List.find (fun (_,t) -> matching_fun (EConstr.of_constr t)) (pf_hyps_types g)
 	in 
+	let t = EConstr.of_constr t in
 	let y = 
-	  let _,args = decompose_app t in 
+	  let _,args = decompose_app sigma t in 
 	  List.hd (List.tl args)
 	in 
 	observe_tclTHENLIST (str "prove_le")[
-	  Proofview.V82.of_tactic (apply(EConstr.of_constr (mkApp(le_trans (),[|x;y;z;mkVar h|]))));
+	  Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|])));
 	  observe_tac (str "prove_le (rec)") (prove_le)
 	] 
       with Not_found -> tclFAIL 0 (mt())
@@ -863,23 +879,24 @@ let rec make_rewrite_list expr_info max = function
     observe_tac (str "make_rewrite_list") (tclTHENS
       (observe_tac (str "rewrite heq on " ++ pr_id p ) (
 	(fun g -> 
+          let sigma = project g in
 	  let t_eq = compute_renamed_type g (mkVar hp) in
 	  let k,def =
-	    let k_na,_,t = destProd t_eq in
-	    let _,_,t  = destProd t in
-	    let def_na,_,_ = destProd t in
+	    let k_na,_,t = destProd sigma t_eq in
+	    let _,_,t  = destProd sigma t in
+	    let def_na,_,_ = destProd sigma t in
 	    Nameops.out_name k_na,Nameops.out_name def_na
 	  in
 	  Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
-	    (EConstr.mkVar hp,
+	    (mkVar hp,
 	     ExplicitBindings[Loc.ghost,NamedHyp def,
-			      EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k,
-			      EConstr.of_constr (f_S max)]) false) g) )
+			      expr_info.f_constr;Loc.ghost,NamedHyp k,
+			      f_S max]) false) g) )
       )
       [make_rewrite_list expr_info max l;
        observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
-	 Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_n_Sm)));
+	 Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm));
 	 observe_tac (str "prove_le(2)") prove_le
        ]
       ] )
@@ -889,20 +906,21 @@ let make_rewrite expr_info l hp max =
     (observe_tac (str "make_rewrite") (make_rewrite_list expr_info max l))
     (observe_tac (str "make_rewrite") (tclTHENS
        (fun g -> 
+          let sigma = project g in
 	  let t_eq = compute_renamed_type g (mkVar hp) in
 	  let k,def =
-	    let k_na,_,t = destProd t_eq in
-	    let _,_,t  = destProd t in
-	    let def_na,_,_ = destProd t in
+	    let k_na,_,t = destProd sigma t_eq in
+	    let _,_,t  = destProd sigma t in
+	    let def_na,_,_ = destProd sigma t in
 	    Nameops.out_name k_na,Nameops.out_name def_na
 	  in
 	 observe_tac (str "general_rewrite_bindings")
 	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
-	    (EConstr.mkVar hp,
+	    (mkVar hp,
 	     ExplicitBindings[Loc.ghost,NamedHyp def,
-			      EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k,
-			      EConstr.of_constr (f_S (f_S max))]) false)) g)
+			      expr_info.f_constr;Loc.ghost,NamedHyp k,
+			      f_S (f_S max)]) false)) g)
        [observe_tac(str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
 	 (observe_tclTHENLIST (str "make_rewrite")[
@@ -931,7 +949,7 @@ let rec compute_max rew_tac max l =
     | (_,p,_)::l -> 
       observe_tclTHENLIST (str "compute_max")[
 	Proofview.V82.of_tactic (simplest_elim 
-	  (EConstr.of_constr (mkApp(delayed_force max_constr, [| max; mkVar p|]))));
+	  (mkApp(delayed_force max_constr, [| max; mkVar p|])));
 	tclDO 3 (Proofview.V82.of_tactic intro);
 	onNLastHypsId 3 (fun lids -> 
 	  match lids with
@@ -950,7 +968,7 @@ let rec destruct_hex expr_info acc l =
       end
     | (v,hex)::l -> 
       observe_tclTHENLIST (str "destruct_hex")[
-	Proofview.V82.of_tactic (simplest_case (EConstr.mkVar hex));
+	Proofview.V82.of_tactic (simplest_case (mkVar hex));
 	Proofview.V82.of_tactic (clear [hex]);
 	tclDO 2 (Proofview.V82.of_tactic intro);
 	onNthHypId 1 (fun hp -> 
@@ -977,36 +995,37 @@ let rec intros_values_eq expr_info acc =
 let equation_others _ expr_info continuation_tac infos = 
   if expr_info.is_final && expr_info.is_main_branch 
   then 
-    observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_lconstr expr_info.info)
+    observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr expr_info.info)
 		(tclTHEN 
       (continuation_tac infos) 
-      (observe_tac (str "intros_values_eq equation_others "  ++ Printer.pr_lconstr expr_info.info) (intros_values_eq expr_info [])))
-  else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_lconstr expr_info.info) (continuation_tac infos)
+      (observe_tac (str "intros_values_eq equation_others "  ++ Printer.pr_leconstr expr_info.info) (intros_values_eq expr_info [])))
+  else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr expr_info.info) (continuation_tac infos)
 
 let equation_app f_and_args expr_info continuation_tac infos = 
     if expr_info.is_final && expr_info.is_main_branch 
     then ((observe_tac (str "intros_values_eq equation_app") (intros_values_eq expr_info [])))
     else continuation_tac infos
 	    
-let equation_app_rec (f,args) expr_info continuation_tac info = 
+let equation_app_rec (f,args) expr_info continuation_tac info g = 
+  let sigma = project g in
   begin
     try
-      let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in
+      let v = List.assoc_f (List.equal (EConstr.eq_constr sigma)) args expr_info.args_assoc in
       let new_infos = {expr_info with info = v} in
-      observe_tac (str "app_rec found") (continuation_tac new_infos)
+      observe_tac (str "app_rec found") (continuation_tac new_infos) g
     with Not_found ->
       if expr_info.is_final && expr_info.is_main_branch 
       then 
 	observe_tclTHENLIST (str "equation_app_rec")
-	  [ Proofview.V82.of_tactic (simplest_case (EConstr.of_constr (mkApp (expr_info.f_terminate,Array.of_list args))));
+	  [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
 	    continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc};
 	    observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info [])
-	  ]
+	  ] g
       else 
 	observe_tclTHENLIST (str "equation_app_rec1")[
-  	  Proofview.V82.of_tactic (simplest_case (EConstr.of_constr (mkApp (expr_info.f_terminate,Array.of_list args))));
+  	  Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
 	  observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc})
-	]
+	] g
   end
 
 let equation_info = 
@@ -1025,6 +1044,8 @@ let prove_eq = travel equation_info
 (* [compute_terminate_type] computes the type of the Definition f_terminate from the type of f_F
 *)
 let compute_terminate_type nb_args func =
+  let open Term in
+  let open CVars in
   let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in
   let rev_args,b = decompose_prod_n nb_args a_arrow_b in
   let left =
@@ -1037,6 +1058,7 @@ let compute_terminate_type nb_args func =
 	 )
   in
   let right = mkRel 5 in
+  let delayed_force c = EConstr.Unsafe.to_constr (delayed_force c) in
   let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in
   let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in
   let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in
@@ -1049,7 +1071,7 @@ let compute_terminate_type nb_args func =
 		  delayed_force nat,
 		  (mkProd (Name k_id, delayed_force nat,
 			   mkArrow cond result))))|])in
-  let value = mkApp(constr_of_global (delayed_force coq_sig_ref),
+  let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref),
 		    [|b;
 		      (mkLambda (Name v_id, b, nb_iter))|]) in
   compose_prod rev_args value
@@ -1089,9 +1111,9 @@ let termination_proof_header is_mes input_type ids args_id relation
 	      (str "first assert")
 	      (Proofview.V82.of_tactic (assert_before
 		 (Name wf_rec_arg)
-		 (EConstr.of_constr (mkApp (delayed_force acc_rel,
+		 (mkApp (delayed_force acc_rel,
 			 [|input_type;relation;mkVar rec_arg_id|])
-		 ))
+		 )
 	      ))
 	   )
 	   [
@@ -1101,7 +1123,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 		  (str "second assert")
 		  (Proofview.V82.of_tactic (assert_before
 		     (Name wf_thm)
-		     (EConstr.of_constr (mkApp (delayed_force well_founded,[|input_type;relation|])))
+		     (mkApp (delayed_force well_founded,[|input_type;relation|]))
 		  ))
 	       )
 	       [
@@ -1110,7 +1132,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 		 (* this gives the accessibility argument *)
 		 observe_tac
 		   (str "apply wf_thm")
-		   (Proofview.V82.of_tactic (Simple.apply (EConstr.of_constr (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))))
+		   (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])))
 		   )
 	       ]
 	     ;
@@ -1119,7 +1141,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       [observe_tac (str "generalize")
 		  (onNLastHypsId (nargs+1)
 		     (tclMAP (fun id ->
-			tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [EConstr.mkVar id])) (Proofview.V82.of_tactic (clear [id])))
+			tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
 		     ))
 	       ;
 		observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1)));
@@ -1133,25 +1155,27 @@ let termination_proof_header is_mes input_type ids args_id relation
 
 
 
-let rec instantiate_lambda t l =
+let rec instantiate_lambda sigma t l =
   match l with
   | [] -> t
   | a::l ->
-      let (_, _, body) = destLambda t in
-      instantiate_lambda (subst1 a body) l
+      let (_, _, body) = destLambda sigma t in
+      instantiate_lambda sigma (subst1 a body) l
 
 let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num  : tactic =
   begin
     fun g ->
+      let sigma = project g in
       let ids = Termops.ids_of_named_context (pf_hyps g) in
       let func_body = (def_of_const (constr_of_global func)) in
-      let (f_name, _, body1) = destLambda func_body in
+      let func_body = EConstr.of_constr func_body in
+      let (f_name, _, body1) = destLambda sigma func_body in
       let f_id =
 	match f_name with
 	  | Name f_id -> next_ident_away_in_goal f_id ids
 	  | Anonymous -> anomaly (Pp.str "Anonymous function")
       in
-      let n_names_types,_ = decompose_lam_n nb_args body1 in
+      let n_names_types,_ = decompose_lam_n sigma nb_args body1 in
       let n_ids,ids =
 	List.fold_left
 	  (fun (n_ids,ids) (n_name,_) ->
@@ -1165,7 +1189,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
 	  n_names_types
       in
       let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in
-      let expr = instantiate_lambda func_body (mkVar f_id::(List.map mkVar n_ids)) in
+      let expr = instantiate_lambda sigma func_body (mkVar f_id::(List.map mkVar n_ids)) in
       termination_proof_header
 	is_mes
 	input_type
@@ -1207,17 +1231,17 @@ let get_current_subgoals_types () =
   let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in
     sigma, List.map (Goal.V82.abstract_type sigma) sgs
 
-let build_and_l l =
+let build_and_l sigma l =
   let and_constr =  Coqlib.build_coq_and () in
   let conj_constr = coq_conj () in
   let mk_and p1 p2 =
-    Term.mkApp(and_constr,[|p1;p2|]) in
+    mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
   let rec is_well_founded t = 
-    match kind_of_term t with 
+    match EConstr.kind sigma t with 
       | Prod(_,_,t') -> is_well_founded t'
       | App(_,_) -> 
-	let (f,_) = decompose_app t in 
-	Term.eq_constr f (well_founded ())
+	let (f,_) = decompose_app sigma t in 
+	EConstr.eq_constr sigma f (well_founded ())
       | _ -> 
 	false
   in
@@ -1248,16 +1272,16 @@ let is_rec_res id =
     String.equal (String.sub id_name 0 (String.length rec_res_name)) rec_res_name
   with Invalid_argument _ -> false
  
-let clear_goals =
+let clear_goals sigma =
   let rec clear_goal t =
-    match kind_of_term t with
+    match EConstr.kind sigma t with
       | Prod(Name id as na,t',b) ->
 	  let b' = clear_goal b in
-	  if noccurn 1 b' && (is_rec_res id)
+	  if noccurn sigma 1 b' && (is_rec_res id)
 	  then Vars.lift (-1) b'
 	  else if b' == b then t
 	  else mkProd(na,t',b')
-      | _ -> Term.map_constr clear_goal t
+      | _ -> EConstr.map sigma clear_goal t
   in
   List.map clear_goal
 
@@ -1265,9 +1289,9 @@ let clear_goals =
 let build_new_goal_type () =
   let sigma, sub_gls_types = get_current_subgoals_types () in
   (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
-  let sub_gls_types = clear_goals sub_gls_types in
+  let sub_gls_types = clear_goals sigma sub_gls_types in
   (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
-  let res = build_and_l sub_gls_types in
+  let res = build_and_l sigma sub_gls_types in
     sigma, res
 
 let is_opaque_constant c =
@@ -1288,7 +1312,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
           anomaly (Pp.str "open_new_goal with an unamed theorem")
   in
   let na = next_global_ident_away name [] in
-  if Termops.occur_existential sigma (EConstr.of_constr gls_type) then
+  if Termops.occur_existential sigma gls_type then
     CErrors.error "\"abstract\" cannot handle existentials";
   let hook _ _ =
     let opacity =
@@ -1299,8 +1323,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
     in
     let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
-    ref_ := Some lemma ;
-    let lemma = EConstr.of_constr lemma in
+    ref_ := Some (EConstr.Unsafe.to_constr lemma);
     let lid = ref [] in
     let h_num = ref (-1) in
     let env = Global.env () in
@@ -1315,7 +1338,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	       (fun g ->
 		  let ids = pf_ids_of_hyps g in
 		  tclTHEN
-		    (Proofview.V82.of_tactic (Elim.h_decompose_and (EConstr.mkVar hid)))
+		    (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)))
 		    (fun g ->
 		       let ids' = pf_ids_of_hyps g in
 		       lid := List.rev (List.subtract Id.equal ids' ids);
@@ -1326,8 +1349,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	       );
 	     ] gls)
       (fun g ->
-	 match kind_of_term (pf_concl g) with
-	   | App(f,_) when Term.eq_constr f (well_founded ()) ->
+        let sigma = project g in
+	 match EConstr.kind sigma (EConstr.of_constr (pf_concl g)) with
+	   | App(f,_) when EConstr.eq_constr sigma f (well_founded ()) ->
 	       Proofview.V82.of_tactic (Auto.h_auto None [] (Some []))  g
 	   | _ ->
 	       incr h_num;
@@ -1336,11 +1360,11 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 		    tclCOMPLETE(
 		      tclFIRST[
 			tclTHEN
-			  (Proofview.V82.of_tactic (eapply_with_bindings (EConstr.mkVar (List.nth !lid !h_num), NoBindings)))
+			  (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
 			  (Proofview.V82.of_tactic e_assumption);
 		      Eauto.eauto_with_bases
 			(true,5)
-			[{ Tacexpr.delayed = fun _ sigma -> Sigma.here (EConstr.of_constr (Lazy.force refl_equal)) sigma}]
+			[{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
 			[Hints.Hint_db.empty empty_transparent_state false]
 		      ]
 		    )
@@ -1353,7 +1377,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
   Lemmas.start_proof
     na
     (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
-    sigma gls_type
+    sigma (EConstr.Unsafe.to_constr gls_type)
     (Lemmas.mk_hook hook);
   if Indfun_common.is_strict_tcc  ()
   then
@@ -1387,7 +1411,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 
 let com_terminate
     tcc_lemma_name
-    tcc_lemma_ref
+    (tcc_lemma_ref : Constr.t option ref)
     is_mes
     fonctional_ref
     input_type
@@ -1424,22 +1448,25 @@ let com_terminate
 
 let start_equation (f:global_reference) (term_f:global_reference)
   (cont_tactic:Id.t list -> tactic) g =
+  let sigma = project g in
   let ids = pf_ids_of_hyps g in
   let terminate_constr = constr_of_global term_f in
-  let nargs = nb_prod (project g) (EConstr.of_constr (fst (type_of_const terminate_constr))) (*FIXME*) in
+  let terminate_constr = EConstr.of_constr terminate_constr in
+  let nargs = nb_prod (project g) (EConstr.of_constr (fst (type_of_const sigma terminate_constr))) (*FIXME*) in
   let x = n_x_id ids nargs in
   observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
     h_intros x;
     Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]);
     observe_tac (str "simplest_case")
-      (Proofview.V82.of_tactic (simplest_case (EConstr.of_constr (mkApp (terminate_constr,
-                             Array.of_list (List.map mkVar x))))));
+      (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
+                             Array.of_list (List.map mkVar x)))));
     observe_tac (str "prove_eq") (cont_tactic x)]) g;;
 
 let (com_eqn : int -> Id.t ->
        global_reference -> global_reference -> global_reference
-	 -> constr -> unit) =
+	 -> Constr.constr -> unit) =
   fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
+    let open CVars in
     let opacity =
       match terminate_ref with
 	| ConstRef c -> is_opaque_constant c
@@ -1459,13 +1486,13 @@ let (com_eqn : int -> Id.t ->
 	  (fun  x ->
 	     prove_eq (fun _ -> tclIDTAC)
 	       {nb_arg=nb_arg;
-		f_terminate = constr_of_global terminate_ref; 
-	        f_constr = f_constr; 
+		f_terminate = EConstr.of_constr (constr_of_global terminate_ref); 
+	        f_constr = EConstr.of_constr f_constr; 
 		concl_tac = tclIDTAC;
 		func=functional_ref;
-		info=(instantiate_lambda
-	       		(def_of_const (constr_of_global functional_ref))
-	       		(f_constr::List.map mkVar x)
+		info=(instantiate_lambda Evd.empty
+	       		(EConstr.of_constr (def_of_const (constr_of_global functional_ref)))
+	       		(EConstr.of_constr f_constr::List.map mkVar x)
 		);
 		is_main_branch = true;
 		is_final = true;
@@ -1491,6 +1518,8 @@ let (com_eqn : int -> Id.t ->
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : unit =
+  let open Term in
+  let open CVars in
   let env = Global.env() in
   let evd = ref (Evd.from_env env) in
   let function_type = interp_type_evars env evd type_of_f in
@@ -1498,8 +1527,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
   let ty = interp_type_evars env evd ~impls:rec_impls eq in
   let evm, nf = Evarutil.nf_evars_and_universes !evd in
-  let equation_lemma_type = nf_betaiotazeta (nf ty) in
+  let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in
   let function_type = nf function_type in
+  let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
  (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
   let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in
@@ -1557,7 +1587,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       and functional_ref = destConst (constr_of_global functional_ref)
       and eq_ref = destConst (constr_of_global eq_ref) in
       generate_induction_principle f_ref tcc_lemma_constr
-	functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod evm (EConstr.of_constr res)) relation;
+	functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation);
       if Flags.is_verbose ()
       then msgnl (h 1 (Ppconstr.pr_id function_name ++
 			 spc () ++ str"is defined" )++ fnl () ++
@@ -1570,8 +1600,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       tcc_lemma_name
       tcc_lemma_constr
       is_mes functional_ref
-      rec_arg_type
-      relation rec_arg_num
+      (EConstr.of_constr rec_arg_type)
+      (EConstr.of_constr relation) rec_arg_num
       term_id
       using_lemmas
       (List.length res_vars)
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index f60eedbe6..9c1081b9d 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -15,6 +15,6 @@ bool ->
            int -> Constrexpr.constr_expr -> (Term.pconstant ->
             Term.constr option ref ->
             Term.pconstant ->
-            Term.pconstant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit
+            Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit
 
 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 7499bc251..410e738de 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -49,7 +49,7 @@ module V82 = struct
   (* Access to ".evar_concl" *)
   let concl evars gl =
     let evi = Evd.find evars gl in
-    evi.Evd.evar_concl
+    EConstr.of_constr evi.Evd.evar_concl
 
   (* Access to ".evar_extra" *)
   let extra evars gl =
@@ -146,6 +146,7 @@ module V82 = struct
 
   (* Goal represented as a type, doesn't take into account section variables *)
   let abstract_type sigma gl =
+    let open EConstr in
     let (gl,sigma) = nf_evar sigma gl in
     let env = env sigma gl in
     let genv = Global.env () in
@@ -159,6 +160,4 @@ module V82 = struct
 					    t
 				       ) ~init:(concl sigma gl) env
 
-  let concl sigma gl = EConstr.of_constr (concl sigma gl)
-
 end
diff --git a/proofs/goal.mli b/proofs/goal.mli
index ca6584e76..a2fa34c05 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -75,6 +75,6 @@ module V82 : sig
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
 
   (* Goal represented as a type, doesn't take into account section variables *)
-  val abstract_type : Evd.evar_map -> goal -> Term.types 
+  val abstract_type : Evd.evar_map -> goal -> EConstr.types 
 
 end