Equality API using EConstr.

22 files changed, 241 insertions, 218 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 9e0a55a0d..1dd9d0c00 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -78,6 +78,8 @@ type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
 type unsafe_type_judgment = types Environ.punsafe_type_judgment
 
+let in_punivs a = (a, Univ.Instance.empty)
+
 let mkProp = of_kind (Sort Sorts.prop)
 let mkSet = of_kind (Sort Sorts.set)
 let mkType u = of_kind (Sort (Sorts.Type u))
@@ -92,8 +94,11 @@ let mkLambda (na, t, c) = of_kind (Lambda (na, t, c))
 let mkLetIn (na, b, t, c) = of_kind (LetIn (na, b, t, c))
 let mkApp (f, arg) = of_kind (App (f, arg))
 let mkConstU pc = of_kind (Const pc)
+let mkConst c = of_kind (Const (in_punivs c))
 let mkIndU pi = of_kind (Ind pi)
+let mkInd i = of_kind (Ind (in_punivs i))
 let mkConstructU pc = of_kind (Construct pc)
+let mkConstruct c = of_kind (Construct (in_punivs c))
 let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
 let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 15463a8f6..e6270fa78 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -62,12 +62,12 @@ val mkProd : Name.t * t * t -> t
 val mkLambda : Name.t * t * t -> t
 val mkLetIn : Name.t * t * t * t -> t
 val mkApp : t * t array -> t
-(* val mkConst : constant -> t *)
+val mkConst : constant -> t
 val mkConstU : pconstant -> t
 val mkProj : (projection * t) -> t
-(* val mkInd : inductive -> t *)
+val mkInd : inductive -> t
 val mkIndU : pinductive -> t
-(* val mkConstruct : constructor -> t *)
+val mkConstruct : constructor -> t
 val mkConstructU : pconstructor -> t
 (* val mkConstructUi : pinductive * int -> t *)
 val mkCase : case_info * t * t * t array -> t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 4f40499d0..c2ad3c462 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -690,29 +690,26 @@ let rec advance sigma evk =
 
 let undefined_evars_of_term evd t =
   let rec evrec acc c =
-    match kind_of_term c with
+    match EConstr.kind evd c with
       | Evar (n, l) ->
-	let acc = Array.fold_left evrec acc l in
-	(try match (Evd.find evd n).evar_body with
-	  | Evar_empty -> Evar.Set.add n acc
-	  | Evar_defined c -> evrec acc c
-	 with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
-      | _ -> fold_constr evrec acc c
+        let acc = Evar.Set.add n acc in
+	Array.fold_left evrec acc l
+      | _ -> EConstr.fold evd evrec acc c
   in
   evrec Evar.Set.empty t
 
 let undefined_evars_of_named_context evd nc =
   Context.Named.fold_outside
-    (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
+    (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd (EConstr.of_constr c))))
     nc
     ~init:Evar.Set.empty
 
 let undefined_evars_of_evar_info evd evi =
-  Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
+  Evar.Set.union (undefined_evars_of_term evd (EConstr.of_constr evi.evar_concl))
     (Evar.Set.union
        (match evi.evar_body with
 	 | Evar_empty -> Evar.Set.empty
-	 | Evar_defined b -> undefined_evars_of_term evd b)
+	 | Evar_defined b -> undefined_evars_of_term evd (EConstr.of_constr b))
        (undefined_evars_of_named_context evd
 	  (named_context_of_val evi.evar_hyps)))
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 6620bbaed..82346b24e 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -121,7 +121,7 @@ val advance : evar_map -> evar -> evar option
     This is roughly a combination of the previous functions and
     [nf_evar]. *)
 
-val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
+val undefined_evars_of_term : evar_map -> EConstr.constr -> Evar.Set.t
 val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
 val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
 
diff --git a/engine/termops.ml b/engine/termops.ml
index b7932665a..c2d862f00 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1074,7 +1074,7 @@ let global_vars_set env sigma constr =
   let rec filtrec acc c =
     let acc = match EConstr.kind sigma c with
     | Var _ | Const _ | Ind _ | Construct _ ->
-      Id.Set.union (vars_of_global env (EConstr.Unsafe.to_constr c)) acc
+      Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc
     | _ -> acc
     in
     EConstr.fold sigma filtrec acc c
diff --git a/engine/termops.mli b/engine/termops.mli
index 7758a57ee..013efcbcb 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -256,6 +256,7 @@ val compact_named_context : Context.Named.t -> Context.Compacted.t
 val clear_named_body : Id.t -> env -> env
 
 val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list
+val global_vars_set : env -> Evd.evar_map -> EConstr.t -> Id.Set.t
 val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t
 val global_app_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses * EConstr.constr option
 
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index faf545d4f..bcfa13c79 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -47,16 +47,16 @@ let with_delayed_uconstr ist c tac =
 
 let replace_in_clause_maybe_by ist c1 c2 cl tac =
   with_delayed_uconstr ist c1
-  (fun c1 -> replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
+  (fun c1 -> replace_in_clause_maybe_by (EConstr.of_constr c1) c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
 
 let replace_term ist dir_opt c cl =
-  with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
+  with_delayed_uconstr ist c (fun c -> replace_term dir_opt (EConstr.of_constr c) cl)
 
 let clause = Pltac.clause_dft_concl
 
 TACTIC EXTEND replace
    ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
--> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
+-> [ replace_in_clause_maybe_by ist c1 (EConstr.of_constr c2) cl tac ]
 END
 
 TACTIC EXTEND replace_term_left
@@ -153,9 +153,9 @@ let injHyp id =
   injection_main false { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma }
 
 TACTIC EXTEND dependent_rewrite
-| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
+| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b (EConstr.of_constr c) ]
 | [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ]
-    -> [ rewriteInHyp b c id ]
+    -> [ rewriteInHyp b (EConstr.of_constr c) id ]
 END
 
 (** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to
@@ -163,9 +163,9 @@ END
     "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *)
 
 TACTIC EXTEND cut_rewrite
-| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
+| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b (EConstr.of_constr eqn) ]
 | [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
-    -> [ cutRewriteInHyp b eqn id ]
+    -> [ cutRewriteInHyp b (EConstr.of_constr eqn) id ]
 END
 
 (**********************************************************************)
@@ -235,7 +235,7 @@ END
 let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) =
   let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in
   with_delayed_uconstr ist c
-    (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true)
+    (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (EConstr.of_constr c,NoBindings) true)
 
 TACTIC EXTEND rewrite_star
 | [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
@@ -719,7 +719,7 @@ let rewrite_except h =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let hyps = Tacmach.New.pf_ids_of_hyps gl in
   Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else 
-      Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
+      Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (EConstr.mkVar h) false))
     hyps
   end }
 
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index ef2ab0917..0d279ae93 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -2094,6 +2094,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 (** Setoid rewriting when called with "rewrite" *)
 let general_s_rewrite cl l2r occs (c,l) ~new_goals =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let (c,l) = Miscops.map_with_bindings EConstr.Unsafe.to_constr (c,l) in
   let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
   let unify env evars t = unify_abs res l2r sort env evars t in
   let app = apply_rule unify occs in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7b023413d..a12ef00ec 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -229,7 +229,8 @@ let make_prb gls depth additionnal_terms =
 
 let build_projection intype (cstr:pconstructor) special default gls=
   let ci= (snd(fst cstr)) in
-  let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+  let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) (EConstr.of_constr default) in
+  let body = EConstr.Unsafe.to_constr body in
   let id=pf_get_new_id (Id.of_string "t") gls in
     mkLambda(Name id,intype,body)
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index fa64b276c..dbb5cc2de 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -600,15 +600,15 @@ let rec fourier () =
 		      (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
 					       else get coq_Rnot_le_le))
 			    (Tacticals.New.tclTHENS (Equality.replace
-				       (mkAppL [|cget coq_Rminus;!t2;!t1|]
-					       )
-				       tc)
+				       (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|]
+					       ))
+				       (EConstr.of_constr tc))
 		 	       [tac2;
                                 (Tacticals.New.tclTHENS
 				  (Equality.replace
-				    (mkApp (cget coq_Rinv,
-				      [|cget coq_R1|]))
-				    (cget coq_R1))
+				    (EConstr.of_constr (mkApp (cget coq_Rinv,
+				      [|cget coq_R1|])))
+				    (get coq_R1))
 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
 
       			        [Tacticals.New.tclORELSE
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 940f1669a..2e3992be9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -401,7 +401,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 (mkVar eq_id))))
+	      (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar eq_id))))
 	      (do_rewrite eq_ids)
 	      g
   in
@@ -1060,7 +1060,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 equation_lemma))
+	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr equation_lemma)))
 		  (revert just_introduced_id) g'
       )
       g
@@ -1425,7 +1425,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 
 let backtrack_eqs_until_hrec hrec eqs : tactic =
   fun gls ->
-    let eqs = List.map mkVar eqs in
+    let eqs = List.map EConstr.mkVar eqs in
     let rewrite =
       tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
     in
@@ -1453,7 +1453,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 (mkVar eq) false)))
+			       true (* dep proofs also: *) true id (EConstr.mkVar eq) false)))
 		    gl
 	       )
 	       eqs
@@ -1659,7 +1659,7 @@ 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 (mkConst eq_ref));
+      Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_ref)));
       (* observe_tac "finish" *) (fun gl' ->
 	 let body =
 	   let _,args = destApp (pf_concl gl') in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a45effb16..08b40a1f7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -502,6 +502,7 @@ let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (G
     | _ -> assert false;;
 
 let list_rewrite (rev:bool) (eqs: (constr*bool) list) =
+  let eqs = List.map (Util.on_fst EConstr.of_constr) eqs in
   tclREPEAT
     (List.fold_right
        (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 36fb6dad3..d29d4694f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -385,7 +385,7 @@ 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 (mkVar hres)));
+	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g ->
 				 Proofview.V82.of_tactic (exact_check (EConstr.of_constr (app_constructor g))) g)  
@@ -520,7 +520,7 @@ 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);
 				     generalize_dependent_of (destVar args.(1)) id;
-				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
@@ -529,7 +529,7 @@ 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);
 				     generalize_dependent_of (destVar args.(2)) id;
-				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
@@ -538,7 +538,7 @@ 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 (mkVar id)));
+			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id)));
 			    intros_with_rewrite
 			  ] g
 			end
@@ -709,7 +709,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 (mkConst eq_lemma));
+	  Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_lemma)));
 	  (* Don't forget to $\zeta$ normlize the term since the principles
              have been $\zeta$-normalized *)
 	  Proofview.V82.of_tactic (reduce
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 74affa396..5cee3cb20 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -871,10 +871,10 @@ let rec make_rewrite_list expr_info max = function
 	  in
 	  Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
-	    (mkVar hp,
+	    (EConstr.mkVar hp,
 	     ExplicitBindings[Loc.ghost,NamedHyp def,
-			      expr_info.f_constr;Loc.ghost,NamedHyp k,
-			      (f_S max)]) false) g) )
+			      EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k,
+			      EConstr.of_constr (f_S max)]) false) g) )
       )
       [make_rewrite_list expr_info max l;
        observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
@@ -898,10 +898,10 @@ let make_rewrite expr_info l hp max =
 	 observe_tac (str "general_rewrite_bindings")
 	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
-	    (mkVar hp,
+	    (EConstr.mkVar hp,
 	     ExplicitBindings[Loc.ghost,NamedHyp def,
-			      expr_info.f_constr;Loc.ghost,NamedHyp k,
-			      (f_S (f_S max))]) false)) g)
+			      EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k,
+			      EConstr.of_constr (f_S (f_S max))]) false)) g)
        [observe_tac(str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
 	 (observe_tclTHENLIST (str "make_rewrite")[
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index b567344c9..d656206d6 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -122,7 +122,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
        Tacticals.New.tclTHEN tac
         (one_base (fun dir c tac ->
 	  let tac = (tac, conds) in
-	    general_rewrite dir AllOccurrences true false ~tac c)
+	    general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c))
 	  tac_main bas))
       (Proofview.tclUNIT()) lbas))
 
@@ -165,7 +165,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
           | _ -> assert false) (* there must be at least an hypothesis *)
      | _ -> assert false (* rewriting cannot complete a proof *)
  in
- let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y z w) in
+ let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y (EConstr.of_constr z) w) in
  Tacticals.New.tclMAP (fun id ->
   Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS
     (List.fold_left (fun tac bas ->
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7d8fc79f4..02211efd6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1315,8 +1315,8 @@ module Intpart = Unionfind.Make(Evar.Set)(Evar.Map)
 
 let deps_of_constraints cstrs evm p =
   List.iter (fun (_, _, x, y) ->
-    let evx = Evarutil.undefined_evars_of_term evm x in
-    let evy = Evarutil.undefined_evars_of_term evm y in
+    let evx = Evarutil.undefined_evars_of_term evm (EConstr.of_constr x) in
+    let evy = Evarutil.undefined_evars_of_term evm (EConstr.of_constr y) in
     Intpart.union_set (Evar.Set.union evx evy) p)
     cstrs
 
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index eb75cbf7d..be9a34239 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -116,7 +116,7 @@ let rec rewrite_and_clear hyps = match hyps with
 | [] -> Proofview.tclUNIT ()
 | id :: hyps ->
   tclTHENLIST [
-    Equality.rewriteLR (mkVar id);
+    Equality.rewriteLR (EConstr.mkVar id);
     clear [id];
     rewrite_and_clear hyps;
   ]
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 80f83f19b..4c79a6199 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -12,8 +12,9 @@ open Util
 open Names
 open Nameops
 open Term
-open Vars
 open Termops
+open EConstr
+open Vars
 open Namegen
 open Inductive
 open Inductiveops
@@ -46,6 +47,10 @@ open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
+let nlocal_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  NamedDecl.LocalAssum (na, inj t)
+
 (* Options *)
 
 let discriminate_introduction = ref true
@@ -144,7 +149,7 @@ let freeze_initial_evars sigma flags clause =
   (* We take evars of the type: this may include old evars! For excluding *)
   (* all old evars, including the ones occurring in the rewriting lemma, *)
   (* we would have to take the clenv_value *)
-  let newevars = Evd.evars_of_term (EConstr.Unsafe.to_constr (clenv_type clause)) in
+  let newevars = Evarutil.undefined_evars_of_term sigma (clenv_type clause) in
   let evars =
     fold_undefined (fun evk _ evars ->
       if Evar.Set.mem evk newevars then evars
@@ -165,11 +170,9 @@ let side_tac tac sidetac =
 
 let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let env = Proofview.Goal.env gl in
-  let c = EConstr.of_constr c in
-  let ty = EConstr.of_constr ty in
-  let l = Miscops.map_bindings EConstr.of_constr l in
+  let sigma = project gl in
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
-  let (equiv, args) = decompose_appvect (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
+  let (equiv, args) = decompose_app_vect sigma (Clenv.clenv_type eqclause) in
   let arglen = Array.length args in
   let () = if arglen < 2 then error "The term provided is not an applied relation." in
   let c1 = args.(arglen - 2) in
@@ -184,11 +187,9 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let c = EConstr.of_constr c in
   let sigma, ct = pf_type_of gl c in
   let ct = EConstr.of_constr ct in
   let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
-  let l = Miscops.map_bindings EConstr.of_constr l in
   let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
   [eqclause]
 
@@ -332,9 +333,9 @@ let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hoo
 let jmeq_same_dom gl = function
   | None -> true (* already checked in Hipattern.find_eq_data_decompose *)
   | Some t ->
-    let rels, t = decompose_prod_assum t in
+    let rels, t = decompose_prod_assum (project gl) t in
     let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in
-    match EConstr.decompose_app (project gl) (EConstr.of_constr t) with
+    match decompose_app (project gl) t with
       | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
       | _ -> false
 
@@ -342,6 +343,8 @@ let jmeq_same_dom gl = function
    eliminate lbeq on sort_of_gl. *)
 
 let find_elim hdcncl lft2rgt dep cls ot gl =
+  let sigma = project gl in
+  let is_global gr c = Termops.is_global sigma gr c in
   let inccl = Option.is_empty cls in
   if (is_global Coqlib.glob_eq hdcncl ||
       (is_global Coqlib.glob_jmeq hdcncl &&
@@ -349,7 +352,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
     || Flags.version_less_or_equal Flags.V8_2
   then
     let c = 
-      match kind_of_term hdcncl with 
+      match EConstr.kind sigma hdcncl with 
       | Ind (ind_sp,u) -> 
 	let pr1 = 
 	  lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) 
@@ -377,6 +380,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	assert false
     in
       let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+      let elim = EConstr.of_constr elim in
       Sigma ((elim, Safe_typing.empty_private_constants), sigma, p)
   else
   let scheme_name = match dep, lft2rgt, inccl with
@@ -391,13 +395,14 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
     | true, _, true -> rew_r2l_dep_scheme_kind
     | true, _, false -> rew_r2l_forward_dep_scheme_kind
   in
-  match kind_of_term hdcncl with
+  match EConstr.kind sigma hdcncl with
   | Ind (ind,u) -> 
       let c, eff = find_scheme scheme_name ind in 
       (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
       let Sigma (elim, sigma, p) =
 	Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
       in
+      let elim = EConstr.of_constr elim in
       Sigma ((elim, eff), sigma, p)
   | _ -> assert false
 
@@ -408,12 +413,12 @@ let type_of_clause cls gl = match cls with
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
-  let isatomic = isProd (whd_zeta evd (EConstr.of_constr hdcncl)) in
+  let isatomic = isProd evd (EConstr.of_constr (whd_zeta evd hdcncl)) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
-  let dep = dep_proof_ok && dep_fun evd (EConstr.of_constr c) (EConstr.of_constr type_of_cls) in
+  let type_of_cls = EConstr.of_constr type_of_cls in
+  let dep = dep_proof_ok && dep_fun evd c type_of_cls in
   let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
-  let elim = EConstr.of_constr elim in
   let tac =
       Proofview.tclEFFECTS effs <*>
       general_elim_clause with_evars frzevars tac cls c t l
@@ -447,11 +452,11 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     Proofview.Goal.enter { enter = begin fun gl ->
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
-    let ctype = get_type_of env sigma (EConstr.of_constr c) in
-    let rels, t = decompose_prod_assum (whd_betaiotazeta sigma (EConstr.of_constr ctype)) in
-      match match_with_equality_type sigma (EConstr.of_constr t) with
+    let ctype = get_type_of env sigma c in
+    let ctype = EConstr.of_constr ctype in
+    let rels, t = decompose_prod_assum sigma (EConstr.of_constr (whd_betaiotazeta sigma ctype)) in
+      match match_with_equality_type sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
-          let hdcncl = EConstr.Unsafe.to_constr hdcncl in
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
 	    l with_evars frzevars dep_proof_ok hdcncl
@@ -465,10 +470,10 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
               | (e, info) ->
                   Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
-	          let rels',t' = splay_prod_assum env' sigma (EConstr.of_constr t) in (* Search for underlying eq *)
-	          match match_with_equality_type sigma (EConstr.of_constr t') with
+	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
+	          let t' = EConstr.of_constr t' in
+	          match match_with_equality_type sigma t' with
 	            | Some (hdcncl,args) ->
-                  let hdcncl = EConstr.Unsafe.to_constr hdcncl in
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		  leibniz_rewrite_ebindings_clause cls lft2rgt tac c
 		    (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl
@@ -533,7 +538,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 	let do_hyps =
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
 	  let ids gl =
-	    let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
+	    let ids_in_c = Termops.global_vars_set (Global.env()) (project gl) (fst c) in
             let ids_of_hyps = pf_ids_of_hyps gl in
 	    Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
 	  in
@@ -563,7 +568,6 @@ let general_multi_rewrite with_evars l cl tac =
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
       let (c, sigma) = run_delayed env sigma f in
-      let c = Miscops.map_with_bindings EConstr.Unsafe.to_constr c in
       tclWITHHOLES with_evars
         (general_rewrite_clause l2r with_evars ?tac c cl) sigma
     end }
@@ -631,12 +635,14 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   in
   Proofview.Goal.enter { enter = begin fun gl ->
   let get_type_of = pf_apply get_type_of gl in
-  let t1 = get_type_of (EConstr.of_constr c1)
-  and t2 = get_type_of (EConstr.of_constr c2) in
+  let t1 = get_type_of c1
+  and t2 = get_type_of c2 in
+  let t1 = EConstr.of_constr t1 in
+  let t2 = EConstr.of_constr t2 in
   let evd = 
     if unsafe then Some (Tacmach.New.project gl)
     else
-      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) (EConstr.of_constr t1) (EConstr.of_constr t2) (Tacmach.New.project gl))
+      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl))
       with Evarconv.UnableToUnify _ -> None
   in
   match evd with
@@ -647,9 +653,9 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
     let sym = build_coq_eq_sym () in
     Tacticals.New.pf_constr_of_global sym (fun sym ->
     Tacticals.New.pf_constr_of_global e (fun e ->
+    let e = EConstr.of_constr e in
     let eq = applist (e, [t1;c1;c2]) in
     let sym = EConstr.of_constr sym in
-    let eq = EConstr.of_constr eq in
     tclTHENLAST
       (replace_core clause l2r eq)
       (tclFIRST
@@ -727,12 +733,10 @@ let _ =
       optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
 let find_positions env sigma t1 t2 =
-  let open EConstr in
   let project env sorts posn t1 t2 =
-    let t1 = EConstr.Unsafe.to_constr t1 in
-    let t2 = EConstr.Unsafe.to_constr t2 in
-    let ty1 = get_type_of env sigma (EConstr.of_constr t1) in
-    let s = get_sort_family_of env sigma (EConstr.of_constr ty1) in
+    let ty1 = get_type_of env sigma t1 in
+    let ty1 = EConstr.of_constr ty1 in
+    let s = get_sort_family_of env sigma ty1 in
     if Sorts.List.mem s sorts
     then [(List.rev posn,t1,t2)] else []
   in
@@ -854,7 +858,7 @@ let injectable env sigma t1 t2 =
 
 let descend_then env sigma head dirn =
   let IndType (indf,_) =
-    try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma (EConstr.of_constr head)))
+    try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma head))
     with Not_found ->
       error "Cannot project on an inductive type derived from a dependency." in
   let indp,_ = (dest_ind_family indf) in
@@ -871,12 +875,12 @@ let descend_then env sigma head dirn =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
 	let result = if Int.equal i dirn then dirnval else dfltval in
-	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in
+	it_mkLambda_or_LetIn result (name_context env cstr.(i-1).cs_args) in
       let brl =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
       let ci = make_case_info env ind RegularStyle in
-      EConstr.Unsafe.to_constr (Inductiveops.make_case_or_project env sigma indf ci (EConstr.of_constr p) (EConstr.of_constr head) (Array.map_of_list EConstr.of_constr brl))))
+      Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
 
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
@@ -897,7 +901,7 @@ let descend_then env sigma head dirn =
 
 let build_selector env sigma dirn c ind special default =
   let IndType(indf,_) =
-    try find_rectype env sigma (EConstr.of_constr ind)
+    try find_rectype env sigma ind
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors
           like T := c : (A:Set)A->T and a discrimination
@@ -909,7 +913,8 @@ let build_selector env sigma dirn c ind special default =
 		 dependent types.") in
   let (indp,_) = dest_ind_family indf in
   let ind, _ = check_privacy env indp in
-  let typ = Retyping.get_type_of env sigma (EConstr.of_constr default) in
+  let typ = Retyping.get_type_of env sigma default in
+  let typ = EConstr.of_constr typ in
   let (mib,mip) = lookup_mind_specif env ind in
   let deparsign = make_arity_signature env true indf in
   let p = it_mkLambda_or_LetIn typ deparsign in
@@ -922,9 +927,14 @@ let build_selector env sigma dirn c ind special default =
   let ci = make_case_info env ind RegularStyle in
   mkCase (ci, p, c, Array.of_list brl)
 
+let build_coq_False () = EConstr.of_constr (build_coq_False ())
+let build_coq_True () = EConstr.of_constr (build_coq_True ())
+let build_coq_I () = EConstr.of_constr (build_coq_I ())
+
 let rec build_discriminator env sigma dirn c = function
   | [] ->
-      let ind = get_type_of env sigma (EConstr.of_constr c) in
+      let ind = get_type_of env sigma c in
+      let ind = EConstr.of_constr ind in
       let true_0,false_0 =
         build_coq_True(),build_coq_False() in
       build_selector env sigma dirn c ind true_0 false_0
@@ -952,7 +962,7 @@ let gen_absurdity id =
   let hyp_typ = EConstr.of_constr hyp_typ in
   if is_empty_type sigma hyp_typ
   then
-    simplest_elim (EConstr.mkVar id)
+    simplest_elim (mkVar id)
   else
     tclZEROMSG (str "Not the negation of an equality.")
   end }
@@ -980,6 +990,7 @@ let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
   let absurd_term  = build_coq_False () in
   let eq_elim, eff = ind_scheme_of_eq lbeq in
   let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
+  let eq_elim = EConstr.of_constr eq_elim in
     sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
     eff
 
@@ -987,8 +998,6 @@ let eq_baseid = Id.of_string "e"
 
 let apply_on_clause (f,t) clause =
   let sigma =  clause.evd in
-  let f = EConstr.of_constr f in
-  let t = EConstr.of_constr t in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
   let argmv =
     (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
@@ -997,19 +1006,14 @@ let apply_on_clause (f,t) clause =
   clenv_fchain ~with_univs:false argmv f_clause clause
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
-  let t = EConstr.Unsafe.to_constr t in
-  let t1 = EConstr.Unsafe.to_constr t1 in
-  let t2 = EConstr.Unsafe.to_constr t2 in
-  let eqn = EConstr.Unsafe.to_constr eqn in
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
+  let e_env = push_named (nlocal_assum (e, t)) env in
   let discriminator =
     build_discriminator e_env sigma dirn (mkVar e) cpath in
   let sigma,(pf, absurd_term), eff = 
     discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
-  let absurd_term = EConstr.of_constr absurd_term in
   let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.tclEFFECTS eff <*>
@@ -1047,19 +1051,20 @@ let onNegatedEquality with_evars tac =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
+    let ccl = EConstr.of_constr ccl in
     let env = Proofview.Goal.env gl in
-    match kind_of_term (hnf_constr env sigma (EConstr.of_constr ccl)) with
-    | Prod (_,t,u) when is_empty_type sigma (EConstr.of_constr u) ->
+    match EConstr.kind sigma (EConstr.of_constr (hnf_constr env sigma ccl)) with
+    | Prod (_,t,u) when is_empty_type sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
-            onEquality with_evars tac (EConstr.mkVar id,NoBindings)))
+            onEquality with_evars tac (mkVar id,NoBindings)))
     | _ ->
         tclZEROMSG (str "Not a negated primitive equality.")
   end }
 
 let discrSimpleClause with_evars = function
   | None -> onNegatedEquality with_evars discrEq
-  | Some id -> onEquality with_evars discrEq (EConstr.mkVar id,NoBindings)
+  | Some id -> onEquality with_evars discrEq (mkVar id,NoBindings)
 
 let discr with_evars = onEquality with_evars discrEq
 
@@ -1073,7 +1078,7 @@ let discrEverywhere with_evars =
       (tclTHEN
 	(tclREPEAT introf)
 	(tryAllHyps
-          (fun id -> tclCOMPLETE (discr with_evars (EConstr.mkVar id,NoBindings)))))
+          (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
      else (* <= 8.2 compat *)
        tryAllHypsAndConcl (discrSimpleClause with_evars))
 (*    (fun gls ->
@@ -1103,9 +1108,10 @@ let find_sigma_data env s = build_sigma_type ()
  *)
 
 let make_tuple env sigma (rterm,rty) lind =
-  assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty)));
-  let sigdata = find_sigma_data env (get_sort_of env sigma (EConstr.of_constr rty)) in
-  let sigma, a = type_of ~refresh:true env sigma (EConstr.mkRel lind) in
+  assert (not (noccurn sigma lind rty));
+  let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
+  let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
+  let a = EConstr.of_constr a in
   let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
   (* We move [lind] to [1] and lift other rels > [lind] by 1 *)
   let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1113,6 +1119,8 @@ let make_tuple env sigma (rterm,rty) lind =
   let p = mkLambda (na, a, rty) in
   let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
   let sigma, sig_term = Evd.fresh_global env sigma sigdata.typ in
+  let exist_term = EConstr.of_constr exist_term in
+  let sig_term = EConstr.of_constr sig_term in
     sigma,
     (applist(exist_term,[a;p;(mkRel lind);rterm]),
      applist(sig_term,[a;p]))
@@ -1125,9 +1133,10 @@ let make_tuple env sigma (rterm,rty) lind =
    normalization *)
 
 let minimal_free_rels env sigma (c,cty) =
-  let cty_rels = free_rels sigma (EConstr.of_constr cty) in
-  let cty' = simpl env sigma (EConstr.of_constr cty) in
-  let rels' = free_rels sigma (EConstr.of_constr cty') in
+  let cty_rels = free_rels sigma cty in
+  let cty' = simpl env sigma cty in
+  let cty' = EConstr.of_constr cty' in
+  let rels' = free_rels sigma cty' in
   if Int.Set.subset cty_rels rels' then
     (cty,cty_rels)
   else
@@ -1139,7 +1148,7 @@ let minimal_free_rels_rec env sigma =
   let rec minimalrec_free_rels_rec prev_rels (c,cty) =
     let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
     let combined_rels = Int.Set.union prev_rels direct_rels in
-    let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (EConstr.mkRel i)))
+    let folder rels i = snd (minimalrec_free_rels_rec rels (c, EConstr.of_constr (unsafe_type_of env sigma (mkRel i))))
     in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
   in minimalrec_free_rels_rec Int.Set.empty
 
@@ -1185,27 +1194,30 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let rec sigrec_clausal_form siglen p_i =
     if Int.equal siglen 0 then
       (* is the default value typable with the expected type *)
-      let dflt_typ = unsafe_type_of env sigma (EConstr.of_constr dflt) in
+      let dflt_typ = unsafe_type_of env sigma dflt in
       try
-	let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) (EConstr.of_constr p_i) !evdref in
+	let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) p_i !evdref in
 	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
 	dflt
       with Evarconv.UnableToUnify _ ->
 	error "Cannot solve a unification problem."
     else
-      let (a,p_i_minus_1) = match whd_beta_stack !evdref (EConstr.of_constr p_i) with
-	| (_sigS,[a;p]) -> (EConstr.Unsafe.to_constr a, EConstr.Unsafe.to_constr p)
+      let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
+	| (_sigS,[a;p]) -> (a, p)
  	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
-      let ev = Evarutil.e_new_evar env evdref (EConstr.of_constr a) in
-      let rty = beta_applist sigma (EConstr.of_constr p_i_minus_1,[ev]) in
+      let ev = Evarutil.e_new_evar env evdref a in
+      let rty = beta_applist sigma (p_i_minus_1,[ev]) in
+      let rty = EConstr.of_constr rty in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
       let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
       match evopt with
 	| Some w ->
             let w_type = unsafe_type_of env !evdref w in
-            if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr a) then
+            let w_type = EConstr.of_constr w_type in
+            if Evarconv.e_cumul env evdref w_type a then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
-              applist(exist_term,[a;p_i_minus_1;EConstr.Unsafe.to_constr w;tuple_tail])
+	      let exist_term = EConstr.of_constr exist_term in
+              applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
               error "Cannot solve a unification problem."
 	| None ->
@@ -1218,7 +1230,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	    error "Cannot solve a unification problem."
   in
   let scf = sigrec_clausal_form siglen ty in
-    !evdref, Evarutil.nf_evar !evdref scf
+    !evdref, EConstr.of_constr (Evarutil.nf_evar !evdref (EConstr.Unsafe.to_constr scf))
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
@@ -1280,18 +1292,18 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 
 let make_iterated_tuple env sigma dflt (z,zty) =
   let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
-  let sort_of_zty = get_sort_of env sigma (EConstr.of_constr zty) in
+  let sort_of_zty = get_sort_of env sigma zty in
   let sorted_rels = Int.Set.elements rels in
   let sigma, (tuple,tuplety) =
     List.fold_left (fun (sigma, t) -> make_tuple env sigma t) (sigma, (z,zty)) sorted_rels
   in
-  assert (closed0 tuplety);
+  assert (closed0 sigma tuplety);
   let n = List.length sorted_rels in
   let sigma, dfltval = sig_clausal_form env sigma sort_of_zty n tuplety dflt in
     sigma, (tuple,tuplety,dfltval)
 
 let rec build_injrec env sigma dflt c = function
-  | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma (EConstr.of_constr c))
+  | [] -> make_iterated_tuple env sigma dflt (c,EConstr.of_constr (unsafe_type_of env sigma c))
   | ((sp,cnum),argnum)::l ->
     try
       let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1326,40 +1338,44 @@ let inject_if_homogenous_dependent_pair ty =
   try
     let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
-    let t = EConstr.Unsafe.to_constr t in
     (* fetch the informations of the  pair *)
     let ceq = Universes.constr_of_global Coqlib.glob_eq in
+    let ceq = EConstr.of_constr ceq in
     let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
     let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in
     (* check whether the equality deals with dep pairs or not *)
-    let eqTypeDest = fst (decompose_app t) in
-    if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit;
+    let eqTypeDest = fst (decompose_app sigma t) in
+    if not (Termops.is_global sigma (sigTconstr()) eqTypeDest) then raise Exit;
     let hd1,ar1 = decompose_app_vect sigma t1 and
         hd2,ar2 = decompose_app_vect sigma t2 in
-    if not (Globnames.is_global (existTconstr()) hd1) then raise Exit;
-    if not (Globnames.is_global (existTconstr()) hd2) then raise Exit;
-    let ind,_ = try pf_apply find_mrectype gl (EConstr.of_constr ar1.(0)) with Not_found -> raise Exit in
+    let hd1 = EConstr.of_constr hd1 in
+    let hd2 = EConstr.of_constr hd2 in
+    let ar1 = Array.map EConstr.of_constr ar1 in
+    let ar2 = Array.map EConstr.of_constr ar2 in
+    if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit;
+    if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit;
+    let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
     (* check if the user has declared the dec principle *)
     (* and compare the fst arguments of the dep pair *)
     (* Note: should work even if not an inductive type, but the table only *)
     (* knows inductive types *)
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
-      pf_apply is_conv gl (EConstr.of_constr ar1.(2)) (EConstr.of_constr ar2.(2))) then raise Exit;
+      pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
-    let new_eq_args = [|pf_unsafe_type_of gl (EConstr.of_constr ar1.(3));ar1.(3);ar2.(3)|] in
+    let new_eq_args = [|EConstr.of_constr (pf_unsafe_type_of gl ar1.(3));ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+    let inj2 = EConstr.of_constr inj2 in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
     (* cut with the good equality and prove the requested goal *)
     tclTHENLIST
       [Proofview.tclEFFECTS eff;
        intro;
        onLastHyp (fun hyp ->
-       let hyp = EConstr.Unsafe.to_constr hyp in
-        tclTHENS (cut (EConstr.of_constr (mkApp (ceq,new_eq_args))))
-          [clear [destVar hyp];
+        tclTHENS (cut (mkApp (ceq,new_eq_args)))
+          [clear [destVar sigma hyp];
            Proofview.V82.tactic (Tacmach.refine
-             (EConstr.of_constr (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
+             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
           ])]
   with Exit ->
     Proofview.tclUNIT ()
@@ -1371,17 +1387,15 @@ let inject_if_homogenous_dependent_pair ty =
 
 let simplify_args env sigma t =
   (* Quick hack to reduce in arguments of eq only *)
-  match decompose_app t with
-    | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma (EConstr.of_constr c1);simpl env sigma (EConstr.of_constr c2)])
-    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma (EConstr.of_constr c1);t2;simpl env sigma (EConstr.of_constr c2)])
+  let simpl env sigma c = EConstr.of_constr (simpl env sigma c) in
+  match decompose_app sigma t with
+    | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma c1;simpl env sigma c2])
+    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2])
     | _ -> t
 
 let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
-  let t = EConstr.Unsafe.to_constr t in
-  let t1 = EConstr.Unsafe.to_constr t1 in
-  let t2 = EConstr.Unsafe.to_constr t2 in
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (LocalAssum (e,t)) env in
+  let e_env = push_named (nlocal_assum (e,t)) env in
   let evdref = ref sigma in
   let filter (cpath, t1', t2') =
     try
@@ -1389,12 +1403,13 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
       let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in
       let injfun = mkNamedLambda e t injbody in
       let sigma,congr = Evd.fresh_global env sigma eq.congr in
+      let congr = EConstr.of_constr congr in
       let pf = applist(congr,[t;resty;injfun;t1;t2]) in
-      let sigma, pf_typ = Typing.type_of env sigma (EConstr.of_constr pf) in
+      let sigma, pf_typ = Typing.type_of env sigma pf in
+      let pf_typ = EConstr.of_constr pf_typ in
       let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
       let pf = Clenvtac.clenv_value_cast_meta inj_clause in
-      let ty = simplify_args env sigma (EConstr.Unsafe.to_constr (clenv_type inj_clause)) in
-      let pf = EConstr.Unsafe.to_constr pf in
+      let ty = simplify_args env sigma (clenv_type inj_clause) in
 	evdref := sigma;
 	Some (pf, ty)
     with Failure _ -> None
@@ -1406,9 +1421,9 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
     (Tacticals.New.tclTHENFIRST
       (Proofview.tclIGNORE (Proofview.Monad.List.map
-         (fun (pf,ty) -> tclTHENS (cut (EConstr.of_constr ty))
-           [inject_if_homogenous_dependent_pair (EConstr.of_constr ty);
-            Proofview.V82.tactic (Tacmach.refine (EConstr.of_constr pf))])
+         (fun (pf,ty) -> tclTHENS (cut ty)
+           [inject_if_homogenous_dependent_pair ty;
+            Proofview.V82.tactic (Tacmach.refine pf)])
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
@@ -1428,7 +1443,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
      tclZEROMSG (str"Nothing to inject.")
   | Inr posns ->
       inject_at_positions env sigma l2r u eq_clause posns
-	(tac (EConstr.Unsafe.to_constr (clenv_value eq_clause)))
+	(tac (clenv_value eq_clause))
 
 let get_previous_hyp_position id gl =
   let rec aux dest = function
@@ -1451,10 +1466,10 @@ let injEq ?(old=false) with_evars clear_flag ipats =
     match ipats_style with
     | Some ipats ->
       Proofview.Goal.enter { enter = begin fun gl ->
-        let destopt = match kind_of_term c with
+        let sigma = project gl in
+        let destopt = match EConstr.kind sigma c with
         | Var id -> get_previous_hyp_position id gl
         | _ -> MoveLast in
-        let c = EConstr.of_constr c in
         let clear_tac =
           tclTRY (apply_clear_request clear_flag dft_clear_flag c) in
         (* Try should be removal if dependency were treated *)
@@ -1488,10 +1503,10 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn
       | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
-        ntac (EConstr.Unsafe.to_constr (clenv_value clause)) 0
+        ntac (clenv_value clause) 0
     | Inr posns ->
 	inject_at_positions env sigma true u clause posns
-          (ntac (EConstr.Unsafe.to_constr (clenv_value clause)))
+          (ntac (clenv_value clause))
   end }
 
 let dEqThen with_evars ntac = function
@@ -1500,7 +1515,6 @@ let dEqThen with_evars ntac = function
 
 let dEq with_evars =
   dEqThen with_evars (fun clear_flag c x ->
-    let c = EConstr.of_constr c in
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
 let intro_decomp_eq tac data (c, t) =
@@ -1547,26 +1561,24 @@ let decomp_tuple_term env sigma c t =
   let rec decomprec inner_code ex exty =
     let iterated_decomp =
     try
-      let ex = EConstr.of_constr ex in
       let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in
-      let a = EConstr.Unsafe.to_constr a in
-      let p = EConstr.Unsafe.to_constr p in
-      let car = EConstr.Unsafe.to_constr car in
-      let cdr = EConstr.Unsafe.to_constr cdr in
       let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code])
       and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in
-      let cdrtyp = beta_applist sigma (EConstr.of_constr p,[EConstr.of_constr car]) in
+      let cdrtyp = beta_applist sigma (p,[car]) in
+      let cdrtyp = EConstr.of_constr cdrtyp in
       List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp)
     with Constr_matching.PatternMatchingFailure ->
       []
     in [((ex,exty),inner_code)]::iterated_decomp
   in decomprec (mkRel 1) c t
 
+let lambda_create env (a,b) =
+  mkLambda (named_hd env (EConstr.Unsafe.to_constr a) Anonymous, a, b)
+
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
-  let dep_pair1 = EConstr.Unsafe.to_constr dep_pair1 in
-  let dep_pair2 = EConstr.Unsafe.to_constr dep_pair2 in
   let sigma = Sigma.to_evar_map sigma in
-  let typ = get_type_of env sigma (EConstr.of_constr dep_pair1) in
+  let typ = get_type_of env sigma dep_pair1 in
+  let typ = EConstr.of_constr typ in
   (* We find all possible decompositions *)
   let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
   let decomps2 = decomp_tuple_term env sigma dep_pair2 typ in
@@ -1581,15 +1593,18 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* We build the expected goal *)
   let abst_B =
     List.fold_right
-      (fun (e,t) body -> lambda_create env (t,subst_term sigma (EConstr.of_constr e) (EConstr.of_constr body))) e1_list b in
-  let pred_body = beta_applist sigma (EConstr.of_constr abst_B, List.map EConstr.of_constr proj_list) in
+      (fun (e,t) body -> lambda_create env (t,EConstr.of_constr (subst_term sigma e body))) e1_list b in
+  let pred_body = beta_applist sigma (abst_B,proj_list) in
+  let pred_body = EConstr.of_constr pred_body in
   let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
-  let expected_goal = beta_applist sigma (EConstr.of_constr abst_B,List.map (fst %> EConstr.of_constr) e2_list) in
+  let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
-  let expected_goal = nf_betaiota sigma (EConstr.of_constr expected_goal) in
+  let expected_goal = EConstr.of_constr expected_goal in
+  let expected_goal = nf_betaiota sigma expected_goal in
+  let expected_goal = EConstr.of_constr expected_goal in
   (* Retype to get universes right *)
-  let sigma, expected_goal_ty = Typing.type_of env sigma (EConstr.of_constr expected_goal) in
-  let sigma, _ = Typing.type_of env sigma (EConstr.of_constr body) in
+  let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
+  let sigma, _ = Typing.type_of env sigma body in
   Sigma.Unsafe.of_pair ((body, expected_goal), sigma)
 
 (* Like "replace" but decompose dependent equalities                      *)
@@ -1598,16 +1613,14 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* on for further iterated sigma-tuples                                   *)
 
 let cutSubstInConcl l2r eqn =
-  let eqn = EConstr.of_constr eqn in
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_concl gl in
+  let typ = EConstr.of_constr typ in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
-  let typ = EConstr.of_constr typ in
-  let expected = EConstr.of_constr expected in
   let tac =
   tclTHENFIRST
     (tclTHENLIST [
@@ -1620,16 +1633,14 @@ let cutSubstInConcl l2r eqn =
   end }
 
 let cutSubstInHyp l2r eqn id =
-  let eqn = EConstr.of_constr eqn in
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_get_hyp_typ id gl in
+  let typ = EConstr.of_constr typ in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
   let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
-  let typ = EConstr.of_constr typ in
-  let expected = EConstr.of_constr expected in
   let tac =
     tclTHENFIRST
     (tclTHENLIST [
@@ -1661,9 +1672,9 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
 let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
 let substClause l2r c cls =
-  let c = EConstr.of_constr c in
   Proofview.Goal.enter { enter = begin fun gl ->
   let eq = pf_apply get_type_of gl c in
+  let eq = EConstr.of_constr eq in
   tclTHENS (cutSubstClause l2r eq cls)
     [Proofview.tclUNIT (); exact_no_check c]
   end }
@@ -1707,7 +1718,7 @@ let restrict_to_eq_and_identity eq = (* compatibility *)
     not (is_global glob_identity eq) 
   then raise Constr_matching.PatternMatchingFailure
 
-exception FoundHyp of (Id.t * EConstr.constr * bool)
+exception FoundHyp of (Id.t * constr * bool)
 
 (* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *)
 let is_eq_x gl x d =
@@ -1779,7 +1790,7 @@ let subst_one_var dep_proof_ok x =
           user_err ~hdr:"Subst"
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	       str".")
-        with FoundHyp (id, c, b) -> (id, EConstr.Unsafe.to_constr c, b) in
+        with FoundHyp res -> res in
       subst_one dep_proof_ok x res
   end }
 
@@ -1811,15 +1822,14 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let find_equations gl =
     let gl = Proofview.Goal.assume gl in
     let env = Proofview.Goal.env gl in
+    let sigma = project gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
     let select_equation_name decl =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose (EConstr.of_constr (NamedDecl.get_type decl)) in
-        let x = EConstr.Unsafe.to_constr x in
-        let y = EConstr.Unsafe.to_constr y in
         let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
-        match kind_of_term x, kind_of_term y with
+        match EConstr.kind sigma x, EConstr.kind sigma y with
         | Var z, _  when not (is_evaluable env (EvalVarRef z)) ->
             Some (NamedDecl.get_id decl)
         | _, Var z when not (is_evaluable env (EvalVarRef z)) ->
@@ -1842,14 +1852,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
     let c = EConstr.of_constr c in
     let _,_,(_,x,y) = find_eq_data_decompose c in
-    let x = EConstr.Unsafe.to_constr x in
-    let y = EConstr.Unsafe.to_constr y in
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-    if Term.eq_constr x y then Proofview.tclUNIT () else
-      match kind_of_term x, kind_of_term y with
-      | Var x', _ when not (occur_term sigma (EConstr.of_constr x) (EConstr.of_constr y)) && not (is_evaluable env (EvalVarRef x')) ->
+    if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
+      match EConstr.kind sigma x, EConstr.kind sigma y with
+      | Var x', _ when not (occur_term sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
           subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
-      | _, Var y' when not (occur_term sigma (EConstr.of_constr y) (EConstr.of_constr x)) && not (is_evaluable env (EvalVarRef y')) ->
+      | _, Var y' when not (occur_term sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
           subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
       | _ ->
           Proofview.tclUNIT ()
@@ -1866,19 +1874,18 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
    or situations like "a = S b, b = S a", or also accidentally unfolding
    let-ins *)
   Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let sigma = project gl in
   let find_eq_data_decompose = find_eq_data_decompose gl in
   let test (_,c) =
     try
       let c = EConstr.of_constr c in
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
-      let x = EConstr.Unsafe.to_constr x in
-      let y = EConstr.Unsafe.to_constr y in
       let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-      if Term.eq_constr x y then failwith "caught";
-      match kind_of_term x with Var x -> x | _ ->
-      match kind_of_term y with Var y -> y | _ -> failwith "caught"
+      if EConstr.eq_constr sigma x y then failwith "caught";
+      match EConstr.kind sigma x with Var x -> x | _ ->
+      match EConstr.kind sigma y with Var y -> y | _ -> failwith "caught"
     with Constr_matching.PatternMatchingFailure -> failwith "caught" in
   let test p = try Some (test p) with Failure _ -> None in
   let hyps = pf_hyps_types gl in
@@ -1892,24 +1899,21 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 
 let cond_eq_term_left c t gl =
   try
-    let t = EConstr.of_constr t in
     let (_,x,_) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl (EConstr.of_constr c) x then true else failwith "not convertible"
+    if pf_conv_x gl c x then true else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term_right c t gl =
   try
-    let t = EConstr.of_constr t in
     let (_,_,x) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl (EConstr.of_constr c) x then false else failwith "not convertible"
+    if pf_conv_x gl c x then false else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
 let cond_eq_term c t gl =
   try
-    let t = EConstr.of_constr t in
     let (_,x,y) = pi3 (find_eq_data_decompose gl t) in
-    if pf_conv_x gl (EConstr.of_constr c) x then true
-    else if pf_conv_x gl (EConstr.of_constr c) y then false
+    if pf_conv_x gl c x then true
+    else if pf_conv_x gl c y then false
     else failwith "not convertible"
   with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
 
@@ -1920,7 +1924,7 @@ let rewrite_assumption_cond cond_eq_term cl =
         let id = NamedDecl.get_id hyp in
 	begin
 	  try
-            let dir = cond_eq_term (NamedDecl.get_type hyp) gl in
+            let dir = cond_eq_term (EConstr.of_constr (NamedDecl.get_type hyp)) gl in
 	    general_rewrite_clause dir false (mkVar id,NoBindings) cl
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
@@ -1946,7 +1950,7 @@ let replace_term dir_opt c  =
 (* Declare rewriting tactic for intro patterns "<-" and "->" *)
 
 let _ =
-  let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars (Miscops.map_with_bindings EConstr.Unsafe.to_constr tac) c in
+  let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars tac c in
   Hook.set Tactics.general_rewrite_clause gmr
 
 let _ = Hook.set Tactics.subst_one subst_one
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 97f51ae20..5467b4af2 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -10,6 +10,7 @@
 open Names
 open Term
 open Evd
+open EConstr
 open Environ
 open Ind_tables
 open Locus
@@ -60,30 +61,30 @@ val general_rewrite_clause :
   orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic
 
 val general_multi_rewrite :
-  evars_flag -> (bool * multi * clear_flag * EConstr.constr with_bindings delayed_open) list ->
+  evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
     clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
 
 val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.tactic option -> unit Proofview.tactic
 val replace    : constr -> constr -> unit Proofview.tactic
 val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic
 
-val discr        : evars_flag -> EConstr.constr with_bindings -> unit Proofview.tactic
+val discr        : evars_flag -> constr with_bindings -> unit Proofview.tactic
 val discrConcl   : unit Proofview.tactic
 val discrHyp     : Id.t -> unit Proofview.tactic
 val discrEverywhere : evars_flag -> unit Proofview.tactic
 val discr_tac    : evars_flag ->
-  EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic
+  constr with_bindings destruction_arg option -> unit Proofview.tactic
 val inj          : intro_patterns option -> evars_flag ->
-  clear_flag -> EConstr.constr with_bindings -> unit Proofview.tactic
+  clear_flag -> constr with_bindings -> unit Proofview.tactic
 val injClause    : intro_patterns option -> evars_flag ->
-  EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic
+  constr with_bindings destruction_arg option -> unit Proofview.tactic
 val injHyp       : clear_flag -> Id.t -> unit Proofview.tactic
 val injConcl     : unit Proofview.tactic
 val simpleInjClause : evars_flag ->
-  EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic
+  constr with_bindings destruction_arg option -> unit Proofview.tactic
 
-val dEq : evars_flag -> EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
 
 val make_iterated_tuple :
   env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
@@ -96,8 +97,8 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
 val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
 val rewriteInConcl : bool -> constr -> unit Proofview.tactic
 
-val discriminable : env -> evar_map -> EConstr.constr -> EConstr.constr -> bool
-val injectable : env -> evar_map -> EConstr.constr -> EConstr.constr -> bool
+val discriminable : env -> evar_map -> constr -> constr -> bool
+val injectable : env -> evar_map -> constr -> constr -> bool
 
 (* Subst *)
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 560e7e43d..c31e86383 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -737,7 +737,7 @@ let secvars_of_idset s =
       else p) s Id.Pred.empty
 
 let secvars_of_constr env c =
-  secvars_of_idset (global_vars_set env c)
+  secvars_of_idset (Environ.global_vars_set env c)
 
 let secvars_of_global env gr =
   secvars_of_idset (vars_of_global_reference env gr)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index c66b356c7..ad2e2fa3b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -113,7 +113,15 @@ let make_inv_predicate env evd indf realargs id status concl =
           if closed0 ti then
 	    (xi,ti,ai)
           else
+            let xi = EConstr.of_constr xi in
+            let ti = EConstr.of_constr ti in
+            let ai = EConstr.of_constr ai in
 	    let sigma, res = make_iterated_tuple env' !evd ai (xi,ti) in
+	    let (xi, ti, ai) = res in
+            let xi = EConstr.Unsafe.to_constr xi in
+            let ti = EConstr.Unsafe.to_constr ti in
+            let ai = EConstr.Unsafe.to_constr ai in
+            let res = (xi, ti, ai) in
 	      evd := sigma; res
 	in
         let eq_term = eqdata.Coqlib.eq in
@@ -334,7 +342,7 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
 
 let projectAndApply as_mode thin avoid id eqname names depids =
   let subst_hyp l2r id =
-    tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id)))
+    tclTHEN (tclTRY(rewriteInConcl l2r (EConstr.mkVar id)))
       (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
   in
   let substHypIfVariable tac id =
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 7759c400c..f8ca8343c 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -338,6 +338,8 @@ so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
 *)
 (* used in the leib -> bool side*)
 let do_replace_lb mode lb_scheme_key aavoid narg p q =
+  let p = EConstr.of_constr p in
+  let q = EConstr.of_constr q in
   let avoid = Array.of_list aavoid in
   let do_arg v offset =
   try
@@ -363,7 +365,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
       )
   in
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl (EConstr.of_constr p)) gl in
+    let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p =
         try
@@ -425,9 +427,11 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   let rec aux l1 l2 =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
+        let t1 = EConstr.of_constr t1 in
+        let t2 = EConstr.of_constr t2 in
         Proofview.Goal.enter { enter = begin fun gl ->
-        let tt1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1) in
-        if Term.eq_constr t1 t2 then aux q1 q2
+        let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
+        if EConstr.eq_constr (Tacmach.New.project gl) t1 t2 then aux q1 q2
         else (
           let u,v = try  destruct_ind tt1
           (* trick so that the good sequence is returned*)
@@ -923,7 +927,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
 	      Equality.general_rewrite_bindings_in true
 	                      Locus.AllOccurrences true false
                               (List.hd !avoid)
-                              ((mkVar (List.hd (List.tl !avoid))),
+                              ((EConstr.mkVar (List.hd (List.tl !avoid))),
                                 NoBindings
                               )
                               true;