Reductionops now return EConstrs.

62 files changed, 328 insertions, 344 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index abaa409bd..879d77de2 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -692,6 +692,9 @@ type meta_type_map = (metavariable * types) list
 
 type meta_value_map = (metavariable * constr) list
 
+let isMetaOf sigma mv c =
+  match EConstr.kind sigma c with Meta mv' -> Int.equal mv mv' | _ -> false
+
 let rec subst_meta bl c =
   match kind_of_term c with
     | Meta i -> (try Int.List.assoc i bl with Not_found -> c)
diff --git a/engine/termops.mli b/engine/termops.mli
index 426b5f34d..1699d600e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -130,6 +130,7 @@ val occur_term : Evd.evar_map -> EConstr.t -> EConstr.t -> bool (** Synonymous o
 (* Substitution of metavariables *)
 type meta_value_map = (metavariable * constr) list
 val subst_meta : meta_value_map -> constr -> constr
+val isMetaOf : Evd.evar_map -> metavariable -> EConstr.constr -> bool
 
 (** Type assignment for metavariables *)
 type meta_type_map = (metavariable * types) list
diff --git a/interp/notation.ml b/interp/notation.ml
index d264a1904..29e5a3bfd 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -615,7 +615,7 @@ let find_scope_class_opt = function
 (* Special scopes associated to arguments of a global reference *)
 
 let rec compute_arguments_classes t =
-  match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t)) with
+  match kind_of_term (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with
     | Prod (_,t,u) ->
 	let cl = try Some (compute_scope_class t) with Not_found -> None in
 	cl :: compute_arguments_classes u
diff --git a/kernel/term.ml b/kernel/term.ml
index 62c161be4..3881cd12d 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -179,8 +179,6 @@ let destMeta c = match kind_of_term c with
   | _ -> raise DestKO
 
 let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false
-let isMetaOf mv c =
-  match kind_of_term c with Meta mv' -> Int.equal mv mv' | _ -> false
 
 (* Destructs a variable *)
 let destVar c = match kind_of_term c with
diff --git a/kernel/term.mli b/kernel/term.mli
index a8d9dfbff..e393adb81 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -98,7 +98,6 @@ val isVarId : Id.t -> constr -> bool
 val isInd  : constr -> bool
 val isEvar : constr -> bool
 val isMeta : constr -> bool
-val isMetaOf : metavariable -> constr -> bool
 val isEvar_or_Meta : constr -> bool
 val isSort : constr -> bool
 val isCast : constr -> bool
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 188d041c1..138400991 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -290,6 +290,7 @@ END
 (* Hint Resolve                                                       *)
 
 open Term
+open EConstr
 open Vars
 open Coqlib
 
@@ -298,23 +299,26 @@ let project_hint pri l2r r =
   let env = Global.env() in
   let sigma = Evd.from_env env in
   let sigma, c = Evd.fresh_global env sigma gr in
-  let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
+  let c = EConstr.of_constr c in
+  let t = Retyping.get_type_of env sigma c in
+  let t = EConstr.of_constr t in
   let t =
-    Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) (EConstr.of_constr t) in
-  let t = EConstr.Unsafe.to_constr t in
-  let sign,ccl = decompose_prod_assum t in
-  let (a,b) = match snd (decompose_app ccl) with
+    Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in
+  let sign,ccl = decompose_prod_assum sigma t in
+  let (a,b) = match snd (decompose_app sigma ccl) with
     | [a;b] -> (a,b)
     | _ -> assert false in
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let c = Reductionops.whd_beta Evd.empty (EConstr.of_constr (mkApp (c, Context.Rel.to_extended_vect 0 sign))) in
+  let p = EConstr.of_constr p in
+  let c = Reductionops.whd_beta sigma (mkApp (c, Array.map EConstr.of_constr (Context.Rel.to_extended_vect 0 sign))) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
   let id =
     Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
   in
   let ctx = Evd.universe_context_set sigma in
+  let c = EConstr.to_constr sigma c in
   let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
     (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
@@ -751,7 +755,6 @@ let  mkCaseEq a  : unit Proofview.tactic =
             let env = Proofview.Goal.env gl in
             (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
             let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) concl in
-            let c = EConstr.of_constr c in
 	    change_concl c
           end };
 	  simplest_case a]
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 4c350b093..c92ddf990 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -247,14 +247,11 @@ end) = struct
     in
     let rec aux env evars ty l =
       let t = Reductionops.whd_all env (goalevars evars) ty in
-      let t = EConstr.of_constr t in
 	match EConstr.kind (goalevars evars) t, l with
 	| Prod (na, ty, b), obj :: cstrs ->
           let b = Reductionops.nf_betaiota (goalevars evars) b in
-          let b = EConstr.of_constr b in
 	  if noccurn (goalevars evars) 1 b (* non-dependent product *) then
 	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
-	    let ty = EConstr.of_constr ty in
 	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
 	    let evars, relty = mk_relty evars env ty obj in
 	    let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
@@ -264,7 +261,6 @@ end) = struct
 	      aux (Environ.push_rel (local_assum (na, ty)) env) evars b cstrs
 	    in
 	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
-	    let ty = EConstr.of_constr ty in
 	    let pred = mkLambda (na, ty, b) in
 	    let liftarg = mkLambda (na, ty, arg) in
 	    let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
@@ -275,7 +271,6 @@ end) = struct
 	  (match finalcstr with
 	  | None | Some (_, None) ->
 	    let t = Reductionops.nf_betaiota (fst evars) ty in
-	    let t = EConstr.of_constr t in
 	    let evars, rel = mk_relty evars env t None in
 	      evars, t, rel, [t, Some rel]
 	  | Some (t, Some rel) -> evars, t, rel, [t, Some rel])
@@ -355,7 +350,7 @@ end) = struct
       if Int.equal n 0 then start evars env prod
       else
         let sigma = goalevars evars in
-	match EConstr.kind sigma (EConstr.of_constr (Reductionops.whd_all env sigma prod)) with
+	match EConstr.kind sigma (Reductionops.whd_all env sigma prod) with
 	| Prod (na, ty, b) ->
 	  if noccurn sigma 1 b then
 	    let b' = lift (-1) b in
@@ -375,7 +370,6 @@ end) = struct
 	with Not_found ->
           let sigma = goalevars evars in
 	  let ty = Reductionops.whd_all env sigma ty in
-	  let ty = EConstr.of_constr ty in
 	  find env (mkApp (c, [| arg |])) (prod_applist sigma ty [arg]) args
     in find env c ty args
 
@@ -513,7 +507,6 @@ let error_no_relation () = error "Cannot find a relation to rewrite."
 let rec decompose_app_rel env evd t = 
   (** Head normalize for compatibility with the old meta mechanism *)
   let t = Reductionops.whd_betaiota evd t in
-  let t = EConstr.of_constr t in
   match EConstr.kind evd t with
   | App (f, [||]) -> assert false
   | App (f, [|arg|]) ->
@@ -1011,7 +1004,7 @@ let unfold_match env sigma sk app =
   | App (f', args) when eq_constant (fst (destConst sigma f')) sk ->
       let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
       let v = EConstr.of_constr v in
-	EConstr.of_constr (Reductionops.whd_beta sigma (mkApp (v, args)))
+	Reductionops.whd_beta sigma (mkApp (v, args))
   | _ -> app
 
 let is_rew_cast = function RewCast _ -> true | _ -> false
@@ -1106,7 +1099,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		      | x -> x
 		    in
 		    let res =
-		      { rew_car = EConstr.of_constr (Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args);
+		      { rew_car = Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args;
 			rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
 			rew_prf = prf; rew_evars = r.rew_evars }
 		    in 
@@ -1455,7 +1448,6 @@ module Strategies =
           let rfn, ckind = Redexpr.reduction_of_red_expr env r in
           let sigma = Sigma.Unsafe.of_evar_map (goalevars evars) in
 	  let Sigma (t', sigma, _) = rfn.Reductionops.e_redfun env sigma t in
-	  let t' = EConstr.of_constr t' in
 	  let evars' = Sigma.to_evar_map sigma in
 	    if Termops.eq_constr evars' t' t then
 	      state, Identity
@@ -1475,7 +1467,6 @@ module Strategies =
 	  with e when CErrors.noncritical e ->
             error "fold: the term is not unfoldable !"
 	in
-	let unfolded = EConstr.of_constr unfolded in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
 	    let c' = nf_evar sigma c in
@@ -1568,7 +1559,6 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
 	| RewCast c -> None
 	| RewPrf (rel, p) ->
 	  let p = nf_zeta env evars' (nf_evar evars' p) in
-	  let p = EConstr.of_constr p in
 	  let term =
 	    match abs with
 	    | None -> p
@@ -1951,8 +1941,7 @@ let declare_projection n instance_id r =
 	  | _ -> typ
       in aux init
     in
-    let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ in
-    let ccl = EConstr.of_constr ccl
+    let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 572fa32b7..6c59abe66 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -785,6 +785,7 @@ let interp_may_eval f ist env sigma = function
       let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
       let sigma = Sigma.Unsafe.of_evar_map sigma in
       let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma (EConstr.of_constr c_interp) in
+      let c = EConstr.Unsafe.to_constr c in
       (Sigma.to_evar_map sigma, c)
   | ConstrContext ((loc,s),c) ->
       (try
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 93bd88fe4..a0b04ce3b 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -182,6 +182,7 @@ module Btauto = struct
     let var = EConstr.of_constr var in
     (* Compute an assignment that dissatisfies the goal *)
     let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
+    let var = EConstr.Unsafe.to_constr var in
     let rec to_list l = match decomp_term (Tacmach.project gl) l with
     | Term.App (c, _)
       when c === (Lazy.force CoqList._nil) -> []
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c3254010a..7123ebcaf 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1103,7 +1103,7 @@ let thesis_for obj typ per_info env=
       ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
 	 str "cannot give an induction hypothesis (wrong parameters).") in
   let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
-    compose_prod rc (Reductionops.whd_beta Evd.empty (EConstr.of_constr hd2))
+    compose_prod rc (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty (EConstr.of_constr hd2)))
 
 let rec build_product_dep pat_info per_info args body gls =
   match args with
@@ -1233,7 +1233,7 @@ let hrec_for fix_id per_info gls obj_id =
     try List.for_all2 Term.eq_constr params per_info.per_params with
         Invalid_argument _ -> false end;
   let hd2 = applist (mkVar fix_id,args@[obj]) in
-    EConstr.of_constr (compose_lam rc (Reductionops.whd_beta gls.sigma (EConstr.of_constr hd2)))
+    EConstr.of_constr (compose_lam rc (EConstr.Unsafe.to_constr (Reductionops.whd_beta gls.sigma (EConstr.of_constr hd2))))
 
 let warn_missing_case =
   CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 460157130..61547f96d 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -70,11 +70,17 @@ type scheme = TypeScheme | Default
 
 type flag = info * scheme
 
+let whd_all env t =
+  EConstr.Unsafe.to_constr (whd_all env none (EConstr.of_constr t))
+
+let whd_betaiotazeta t =
+  EConstr.Unsafe.to_constr (whd_betaiotazeta none (EConstr.of_constr t))
+
 (*s [flag_of_type] transforms a type [t] into a [flag].
   Really important function. *)
 
 let rec flag_of_type env t : flag =
-  let t = whd_all env none (EConstr.of_constr t) in
+  let t = whd_all env t in
   match kind_of_term t with
     | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
     | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
@@ -105,14 +111,14 @@ let push_rel_assum (n, t) env =
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
 let rec type_sign env c =
-  match kind_of_term (whd_all env none (EConstr.of_constr c)) with
+  match kind_of_term (whd_all env c) with
     | Prod (n,t,d) ->
 	(if is_info_scheme env t then Keep else Kill Kprop)
 	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
 let rec type_scheme_nb_args env c =
-  match kind_of_term (whd_all env none (EConstr.of_constr c)) with
+  match kind_of_term (whd_all env c) with
     | Prod (n,t,d) ->
 	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
 	if is_info_scheme env t then n+1 else n
@@ -138,7 +144,7 @@ let make_typvar n vl =
   next_ident_away id' vl
 
 let rec type_sign_vl env c =
-  match kind_of_term (whd_all env none (EConstr.of_constr c)) with
+  match kind_of_term (whd_all env c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
 	if not (is_info_scheme env t) then Kill Kprop::s, vl
@@ -146,7 +152,7 @@ let rec type_sign_vl env c =
     | _ -> [],[]
 
 let rec nb_default_params env c =
-  match kind_of_term (whd_all env none (EConstr.of_constr c)) with
+  match kind_of_term (whd_all env c) with
     | Prod (n,t,d) ->
 	let n = nb_default_params (push_rel_assum (n,t) env) d in
 	if is_default env t then n+1 else n
@@ -217,7 +223,7 @@ let parse_ind_args si args relmax =
 
 
 let rec extract_type env db j c args =
-  match kind_of_term (whd_betaiotazeta none (EConstr.of_constr c)) with
+  match kind_of_term (whd_betaiotazeta c) with
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type env db j d (Array.to_list args' @ args)
@@ -319,7 +325,7 @@ and extract_type_app env db (r,s) args =
 and extract_type_scheme env db c p =
   if Int.equal p 0 then extract_type env db 0 c []
   else
-    let c = whd_betaiotazeta none (EConstr.of_constr c) in
+    let c = whd_betaiotazeta c in
     match kind_of_term c with
       | Lambda (n,t,d) ->
           extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
@@ -492,7 +498,7 @@ and extract_really_ind env kn mib =
 *)
 
 and extract_type_cons env db dbmap c i =
-  match kind_of_term (whd_all env none (EConstr.of_constr c)) with
+  match kind_of_term (whd_all env c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
 	let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a320b47aa..24d4346d9 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t=
       let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in
+      let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap (EConstr.of_constr typ))) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 205cb282d..5520c7e35 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -42,8 +42,8 @@ let unif t1 t2=
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
-      let nt1=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t1))
-      and nt2=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t2)) in
+      let nt1=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t1)))
+      and nt2=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t2))) in
 	match (kind_of_term nt1),(kind_of_term nt2) with
 	    Meta i,Meta j->
 	      if not (Int.equal i j) then
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2e3992be9..188368082 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -321,6 +321,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
     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
     let new_ctxt,new_end_of_type =
       decompose_prod_n_assum ctxt_size new_type_of_hyp
     in
@@ -619,6 +620,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 		   )
 	 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_infos =
 	   {dyn_infos with
 	      info = new_body;
@@ -752,6 +754,7 @@ let build_proof
 			     pf_nf_betaiota g'
 			       (EConstr.of_constr (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
@@ -796,6 +799,7 @@ let build_proof
 		  | 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
 		      build_proof do_finalize {dyn_infos with info = new_term}
 			g
 		  | LetIn _ ->
@@ -1097,11 +1101,11 @@ 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 ->
-	     Tacred.cbv_norm_flags
+	     EConstr.Unsafe.to_constr (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
@@ -1152,9 +1156,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    let bodies_with_all_params =
 	      Array.map
 		(fun body ->
-		   Reductionops.nf_betaiota Evd.empty
+		   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)))
+			      List.rev_map var_of_decl princ_params))))
 		)
 		bodies
 	    in
@@ -1190,12 +1194,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		   let body_with_param,num =
 		     let body = get_body fnames.(i) in
 		     let body_with_full_params =
-		       Reductionops.nf_betaiota Evd.empty (EConstr.of_constr (
-			 applist(body,List.rev_map var_of_decl full_params)))
+		       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty (EConstr.of_constr (
+			 applist(body,List.rev_map var_of_decl full_params))))
 		     in
 		     match kind_of_term body_with_full_params with
 		       | Fix((_,num),(_,_,bs)) ->
-			       Reductionops.nf_betaiota Evd.empty
+			       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
 				 (EConstr.of_constr (
 				   (applist
 				      (substl
@@ -1203,7 +1207,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 					    (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 =
@@ -1279,8 +1283,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-		       Reductionops.nf_betaiota Evd.empty
-			 (EConstr.of_constr (applist(fix_body,List.rev_map mkVar args_id)));
+		       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
+			 (EConstr.of_constr (applist(fix_body,List.rev_map mkVar args_id))));
 		     eq_hyps = []
 		   }
 		 in
@@ -1339,11 +1343,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-		       Reductionops.nf_betaiota Evd.empty
+		       EConstr.Unsafe.to_constr (Reductionops.nf_betaiota Evd.empty
 			 (EConstr.of_constr (applist(fbody_with_full_params,
 				  (List.rev_map var_of_decl princ_params)@
 				    (List.rev_map mkVar args_id)
-				 )));
+				 ))));
 		     eq_hyps = []
 		   }
 		 in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 4d88f9f91..b4eb77870 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -409,6 +409,7 @@ let get_funs_constant mp dp =
 	      (Evd.from_env (Global.env ()))
 	      (EConstr.of_constr body)
 	    in
+	    let body = EConstr.Unsafe.to_constr body in
 	    body
 	| None -> error ( "Cannot define a principle over an axiom ")
     in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d29d4694f..c02b64c1f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -252,7 +252,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     (* 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 = EConstr.of_constr 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
@@ -429,7 +428,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
-	     (nf_zeta (EConstr.of_constr p))::bindings,id::avoid)
+	     (EConstr.Unsafe.to_constr (nf_zeta (EConstr.of_constr p)))::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
@@ -662,7 +661,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
     let graph_principle = nf_zeta (EConstr.of_constr schemes.(i))  in
-    let princ_type = pf_unsafe_type_of g (EConstr.of_constr graph_principle) in
+    let princ_type = pf_unsafe_type_of g graph_principle in
     let princ_type = EConstr.of_constr princ_type in
     let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
     (* Then we get the number of argument of the function
@@ -754,14 +753,15 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	g
     in
     let params_names = fst (List.chop princ_infos.nparams args_names) in
+    let open EConstr in
     let params = List.map mkVar params_names in
     tclTHENSEQ
       [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
-	(Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas))]));
+	(Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
 	Proofview.V82.of_tactic (Simple.intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (EConstr.mkVar hres,NoBindings) (Some (EConstr.mkVar graph_principle_id,NoBindings)))))
+	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
@@ -796,6 +796,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_of_lemma = Termops.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);
 	   type_of_lemma,type_info
 	)
@@ -863,6 +864,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	   Termops.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);
 	 type_of_lemma,type_info
 	)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5cee3cb20..c71174fef 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -695,7 +695,7 @@ let mkDestructEq :
         let changefun patvars = { run = fun sigma ->
           let redfun = pattern_occs [Locus.AllOccurrencesBut [1], EConstr.of_constr expr] in
           let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2)) in
-          Sigma (EConstr.of_constr c, sigma, p)
+          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
@@ -1503,6 +1503,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   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
   let eq' = nf_zeta env_eq' (EConstr.of_constr eq') in
+  let eq' = EConstr.Unsafe.to_constr eq' in
   let res =
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
 (*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 72290e681..51790f4c9 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -568,7 +568,7 @@ let abstract_path typ path t =
   mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur
 
 let focused_simpl path gl =
-  let newc = context (fun i t -> pf_nf gl (EConstr.of_constr t)) (List.rev path) (pf_concl gl) in
+  let newc = context (fun i t -> EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr t))) (List.rev path) (pf_concl gl) in
   let newc = EConstr.of_constr newc in
   Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
 
@@ -1386,7 +1386,7 @@ let destructure_omega gl tac_def (id,c) =
   else
     try match destructurate_prop c with
       | Kapp(Eq,[typ;t1;t2])
-	when begin match destructurate_type (pf_nf gl (EConstr.of_constr typ)) with Kapp(Z,[]) -> true | _ -> false end ->
+	when begin match destructurate_type (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) with Kapp(Z,[]) -> true | _ -> false end ->
 	  let t = mk_plus t1 (mk_inv t2) in
 	  normalize_equation
 	    id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
@@ -1661,7 +1661,7 @@ let rec decidability gl t =
     | Kapp(Not,[t1]) ->
         mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |])
     | Kapp(Eq,[typ;t1;t2]) ->
-	begin match destructurate_type (pf_nf gl (EConstr.of_constr typ)) with
+	begin match destructurate_type (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) with
           | Kapp(Z,[]) ->  mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
           | Kapp(Nat,[]) ->  mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
           | _ -> raise Undecidable
@@ -1791,7 +1791,7 @@ let destructure_hyps =
 		   with Not_found -> loop lit)
 	      | Kapp(Eq,[typ;t1;t2]) ->
                   if !old_style_flag then begin
-		    match destructurate_type (pf_nf (EConstr.of_constr typ)) with
+		    match destructurate_type (EConstr.Unsafe.to_constr (pf_nf (EConstr.of_constr typ))) with
 		    | Kapp(Nat,_) ->
                         Tacticals.New.tclTHENLIST [
 			  (simplest_elim
@@ -1808,7 +1808,7 @@ let destructure_hyps =
                         ]
 		    | _ -> loop lit
                   end else begin
-		    match destructurate_type (pf_nf (EConstr.of_constr typ)) with
+		    match destructurate_type (EConstr.Unsafe.to_constr (pf_nf (EConstr.of_constr typ))) with
 		    | Kapp(Nat,_) ->
                         (Tacticals.New.tclTHEN
 			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index f2d91bad3..5c68078d7 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -353,7 +353,7 @@ let parse_term t =
 let parse_rel gl t =
   try match destructurate t with
     | Kapp("eq",[typ;t1;t2])
-      when destructurate (Tacmach.pf_nf gl (EConstr.of_constr typ)) = Kapp("Z",[]) -> Req (t1,t2)
+      when destructurate (EConstr.Unsafe.to_constr (Tacmach.pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2)
     | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
     | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
     | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 4492b854b..b720b2e0a 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -83,8 +83,8 @@ let lookup_map map =
 
 let protect_red map env sigma c =
   let c = EConstr.Unsafe.to_constr c in
-  kl (create_clos_infos all env)
-    (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
+  EConstr.of_constr (kl (create_clos_infos all env)
+    (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c));;
 
 let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 76ced2b1d..c0141f011 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1057,7 +1057,6 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
   (* Note: applying the substitution in tms is not important (is it sure?) *)
   let ccl'' =
     whd_betaiota Evd.empty (subst_predicate (realargsi, copti) ccl' tms) in
-  let ccl'' = EConstr.of_constr ccl'' in
   (* We adjust ccl st: gamma, x'1..x'n, x1..xn, tms |- ccl'' *)
   let ccl''' = liftn_predicate n (n+1) ccl'' tms in
   (* We finally get gamma,x'1..x'n,x |- [X1;x1:I(X1)]..[Xn;xn:I(Xn)]pred'''*)
@@ -1065,8 +1064,8 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
   let pred = abstract_predicate env !evdref indf current realargs dep tms p in
-  (pred, EConstr.of_constr (whd_betaiota !evdref
-           (applist (pred, realargs@[current]))))
+  (pred, whd_betaiota !evdref
+           (applist (pred, realargs@[current])))
 
 (* Take into account that a type has been discovered to be inductive, leading
    to more dependencies in the predicate if the type has indices *)
@@ -1221,7 +1220,7 @@ let rec generalize_problem names pb = function
       | LocalDef (Anonymous,_,_) -> pb', deps
       | _ ->
 	 (* for better rendering *)
-	let d = RelDecl.map_type (fun c -> whd_betaiota !(pb.evdref) (EConstr.of_constr c)) d in
+	let d = RelDecl.map_type (fun c -> EConstr.Unsafe.to_constr (whd_betaiota !(pb.evdref) (EConstr.of_constr c))) d in
         let tomatch = lift_tomatch_stack 1 pb'.tomatch in
         let tomatch = relocate_index_tomatch !(pb.evdref) (i+1) 1 tomatch in
         { pb' with
@@ -1400,7 +1399,6 @@ and match_current pb (initial,tomatch) =
 	      pred current indt (names,dep) tomatch in
 	  let ci = make_case_info pb.env (fst mind) pb.casestyle in
 	  let pred = nf_betaiota !(pb.evdref) pred in
-	  let pred = EConstr.of_constr pred in
 	  let case =
 	    make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
 	  in
@@ -1638,7 +1636,6 @@ let rec list_assoc_in_triple x = function
 
 let abstract_tycon loc env evdref subst tycon extenv t =
   let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*)
-  let t = EConstr.of_constr t in
   let src = match EConstr.kind !evdref t with
     | Evar (evk,_) -> (loc,Evar_kinds.SubEvar evk)
     | _ -> (loc,Evar_kinds.CasesType true) in
@@ -1734,7 +1731,7 @@ let build_inversion_problem loc env sigma tms t =
     let id = next_name_away (named_hd env (EConstr.Unsafe.to_constr t) Anonymous) avoid in
     PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
-    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+    match EConstr.kind sigma (whd_all env sigma t) with
     | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc
     | App (f,v) when isConstruct sigma f ->
 	let cstr,u = destConstruct sigma f in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 23d20dad3..e4331aade 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -234,7 +234,6 @@ let class_of env sigma t =
       (t, n1, i, u, args)
     with Not_found ->
       let t = Tacred.hnf_constr env sigma t in
-      let t = EConstr.of_constr t in
       let (cl, u, args) = find_class_type sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, u, args)
@@ -279,7 +278,6 @@ let apply_on_class_of env sigma t cont =
   with Not_found ->
     (* Is it worth to be more incremental on the delta steps? *)
     let t = Tacred.hnf_constr env sigma t in
-    let t = EConstr.of_constr t in
     let (cl, u, args) = find_class_type sigma t in
     let (i, { cl_param = n1 } ) = class_info cl in
     if not (Int.equal (List.length args) n1) then raise Not_found;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 48f7be4bb..7e8559630 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -64,7 +64,7 @@ let apply_coercion_args env evd check isproj argl funj =
 	{ uj_val = applist (j_val funj,argl);
 	  uj_type = typ }
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
-      match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
+      match EConstr.kind !evdref (whd_all env !evdref typ) with
       | Prod (_,c1,c2) ->
         if check && not (e_cumul env evdref (EConstr.of_constr (Retyping.get_type_of env !evdref h)) c1) then
 	  raise NoCoercion;
@@ -96,7 +96,7 @@ let make_existential loc ?(opaque = not (get_proofs_transparency ()))  env evdre
   Evarutil.e_new_evar env evdref ~src c
 
 let app_opt env evdref f t =
-  EConstr.of_constr (whd_betaiota !evdref (app_opt f t))
+  whd_betaiota !evdref (app_opt f t)
 
 let pair_of_array a = (a.(0), a.(1))
 
@@ -134,11 +134,10 @@ let local_assum (na, t) =
 let mu env evdref t =
   let rec aux v =
     let v' = hnf env !evdref v in
-    let v' = EConstr.of_constr v' in
       match disc_subset !evdref v' with
       | Some (u, p) ->
 	let f, ct = aux u in
-	let p = EConstr.of_constr (hnf_nodelta env !evdref p) in
+	let p = hnf_nodelta env !evdref p in
 	  (Some (fun x ->
 		   app_opt env evdref 
 		     f (papp evdref sig_proj1 [| u; p; x |])),
@@ -152,8 +151,6 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
   let open Context.Rel.Declaration in
   let rec coerce_unify env x y =
     let x = hnf env !evdref x and y = hnf env !evdref y in
-    let x = EConstr.of_constr x in
-    let y = EConstr.of_constr y in
       try
 	evdref := the_conv_x_leq env x y !evdref;
 	None
@@ -162,7 +159,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
     let subco () = subset_coerce env evdref x y in
     let dest_prod c =
       match Reductionops.splay_prod_n env (!evdref) 1 c with
-      | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, EConstr.of_constr t), EConstr.of_constr c
+      | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, EConstr.of_constr t), c
       | _ -> raise NoSubtacCoercion
     in
     let coerce_application typ typ' c c' l l' =
@@ -344,7 +341,7 @@ let app_coercion env evdref coercion v =
   | None -> v
   | Some f ->
      let v' = Typing.e_solve_evars env evdref (f v) in
-     EConstr.of_constr (whd_betaiota !evdref (EConstr.of_constr v'))
+     whd_betaiota !evdref (EConstr.of_constr v')
 
 let coerce_itf loc env evd v t c1 =
   let evdref = ref evd in
@@ -381,7 +378,6 @@ let apply_coercion env sigma p hj typ_cl =
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
 let inh_app_fun_core env evd j =
   let t = whd_all env evd j.uj_type in
-  let t = EConstr.of_constr t in
     match EConstr.kind evd t with
     | Prod (_,_,_) -> (evd,j)
     | Evar ev ->
@@ -413,7 +409,7 @@ let inh_app_fun resolve_tc env evd j =
     with NoCoercion -> (evd, j)
 
 let type_judgment env sigma j =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma j.uj_type)) with
+  match EConstr.kind sigma (whd_all env sigma j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_a_type env sigma j
 
@@ -429,7 +425,7 @@ let inh_tosort_force loc env evd j =
 
 let inh_coerce_to_sort loc env evd j =
   let typ = whd_all env evd j.uj_type in
-    match EConstr.kind evd (EConstr.of_constr typ) with
+    match EConstr.kind evd typ with
     | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
     | Evar ev ->
 	let (evd',s) = Evardefine.define_evar_as_sort env evd ev in
@@ -480,8 +476,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
       match
-      EConstr.kind evd (EConstr.of_constr (whd_all env evd t)),
-      EConstr.kind evd (EConstr.of_constr (whd_all env evd c1))
+      EConstr.kind evd (whd_all env evd t),
+      EConstr.kind evd (whd_all env evd c1)
       with
       | Prod (name,t1,t2), Prod (_,u1,u2) ->
           (* Conversion did not work, we may succeed with a coercion. *)
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 3babc48a7..d4b46c046 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -39,7 +39,7 @@ let env_nf_evar sigma env =
 let env_nf_betaiotaevar sigma env =
   process_rel_context
     (fun d e ->
-      push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma (EConstr.of_constr c)) d) e) env
+      push_rel (RelDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma (EConstr.of_constr c))) d) e) env
 
 (****************************************)
 (* Operations on value/type constraints *)
@@ -85,7 +85,6 @@ let define_pure_evar_as_product evd evk =
   let evenv = evar_env evi in
   let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
   let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
-  let concl = EConstr.of_constr concl in
   let s = destSort evd concl in
   let evd1,(dom,u1) =
     let evd = Sigma.Unsafe.of_evar_map evd in
@@ -138,7 +137,7 @@ let define_pure_evar_as_lambda env evd evk =
   let open Context.Named.Declaration in
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
-  let typ = EConstr.of_constr (Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi))) in
+  let typ = Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi)) in
   let evd1,(na,dom,rng) = match EConstr.kind evd typ with
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
@@ -177,7 +176,6 @@ let define_evar_as_sort env evd (ev,args) =
   let evi = Evd.find_undefined evd ev in 
   let s = Type u in
   let concl = Reductionops.whd_all (evar_env evi) evd (EConstr.of_constr evi.evar_concl) in
-  let concl = EConstr.of_constr concl in
   let sort = destSort evd concl in
   let evd' = Evd.define ev (Constr.mkSort s) evd in
   Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
@@ -190,7 +188,7 @@ let define_evar_as_sort env evd (ev,args) =
 let split_tycon loc env evd tycon =
   let rec real_split evd c =
     let t = Reductionops.whd_all env evd c in
-      match EConstr.kind evd (EConstr.of_constr t) with
+      match EConstr.kind evd t with
 	| Prod (na,dom,rng) -> evd, (na, dom, rng)
 	| Evar ev (* ev is undefined because of whd_all *) ->
 	    let (evd',prod) = define_evar_as_product evd ev in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 65b6d287d..27436fdd8 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -149,7 +149,7 @@ let recheck_applications conv_algo env evdref t =
        let argsty = Array.map (fun x -> aux env x; EConstr.of_constr (Retyping.get_type_of env !evdref x)) args in
        let rec aux i ty =
 	 if i < Array.length argsty then
-	 match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref ty)) with
+	 match EConstr.kind !evdref (whd_all env !evdref ty) with
 	 | Prod (na, dom, codom) ->
 	    (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
 	     | Success evd -> evdref := evd;
@@ -814,7 +814,7 @@ let rec do_projection_effects define_fun env ty evd = function
       let evd = Evd.define evk (Constr.mkVar id) evd in
       (* TODO: simplify constraints involving evk *)
       let evd = do_projection_effects define_fun env ty evd p in
-      let ty = EConstr.of_constr (whd_all env evd (Lazy.force ty)) in
+      let ty = whd_all env evd (Lazy.force ty) in
       if not (isSort evd ty) then
         (* Don't try to instantiate if a sort because if evar_concl is an
            evar it may commit to a univ level which is not the right
@@ -1494,7 +1494,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
 					imitate envk t
   in
-  let rhs = EConstr.of_constr (whd_beta evd rhs) (* heuristic *) in
+  let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
     let names = ref Idset.empty in
@@ -1576,7 +1576,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
         raise e
     | OccurCheckIn (evd,rhs) ->
         (* last chance: rhs actually reduces to ev *)
-        let c = EConstr.of_constr (whd_all env evd rhs) in
+        let c = whd_all env evd rhs in
         match EConstr.kind evd c with
         | Evar (evk',argsv2) when Evar.equal evk evk' ->
 	    solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
@@ -1637,7 +1637,7 @@ let reconsider_conv_pbs conv_algo evd =
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
-    let t2 = EConstr.of_constr (whd_betaiota evd t2) in (* includes whd_evar *)
+    let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
     let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
       reconsider_conv_pbs conv_algo evd
   with
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 4fa5ad06d..1adeb4db2 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -173,6 +173,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	      base
       	| _ ->
 	   let t' = whd_all env sigma (EConstr.of_constr p) in
+	   let t' = EConstr.Unsafe.to_constr t' in
 	   if Term.eq_constr p' t' then assert false
 	   else prec env i sign t'
     in
@@ -247,6 +248,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
             applist(lift i fk,realargs@[arg])
      	| _ ->
 	   let t' = whd_all env sigma (EConstr.of_constr p) in
+	   let t' = EConstr.Unsafe.to_constr t' in
 	     if Term.eq_constr t' p' then assert false
 	     else prec env i hyps t'
     in
@@ -265,7 +267,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
            | None ->
 	       mkLambda_name env
 		 (n,t,process_constr (push_rel d env) (i+1)
-		    (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)]))))
+		    (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)])))))
 		    (cprest,rest))
            | Some(_,f_0) ->
 	       let nF = lift (i+1+decF) f_0 in
@@ -273,7 +275,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	       let arg = process_pos env' nF (lift 1 t) in
                mkLambda_name env
 		 (n,t,process_constr env' (i+1)
-		    (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg]))))
+		    (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg])))))
 		    (cprest,rest)))
     | (LocalDef (n,c,t) as d)::cprest, rest ->
 	mkLetIn
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 9c5a2e894..120adb9fe 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -456,7 +456,7 @@ let extract_mrectype sigma t =
 
 let find_mrectype_vect env sigma c =
   let open EConstr in
-  let (t, l) = Termops.decompose_app_vect sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
     | _ -> raise Not_found
@@ -466,7 +466,7 @@ let find_mrectype env sigma c =
 
 let find_rectype env sigma c =
   let open EConstr in
-  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind (ind,u as indu) ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -478,7 +478,7 @@ let find_rectype env sigma c =
 
 let find_inductive env sigma c =
   let open EConstr in
-  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
@@ -488,7 +488,7 @@ let find_inductive env sigma c =
 
 let find_coinductive env sigma c =
   let open EConstr in
-  let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind
         when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
@@ -503,7 +503,7 @@ let find_coinductive env sigma c =
 
 let is_predicate_explicitly_dep env sigma pred arsign =
   let rec srec env pval arsign =
-    let pv' = EConstr.of_constr (whd_all env sigma pval) in
+    let pv' = whd_all env sigma pval in
     match EConstr.kind sigma pv', arsign with
       | Lambda (na,t,b), (LocalAssum _)::arsign ->
 	  srec (push_rel_assum (na, t) env) b arsign
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index cdaa4e9ee..0228f63cd 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -404,7 +404,7 @@ let native_norm env sigma c ty =
         let t2 = Sys.time () in
         let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
         if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
-        res
+        EConstr.of_constr res
     | _ -> anomaly (Pp.str "Compilation failure") 
 
 let native_conv_generic pb sigma t =
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index ba46138a4..c899340c8 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -12,7 +12,7 @@ open Evd
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-val native_norm : env -> evar_map -> constr -> types -> Constr.t
+val native_norm : env -> evar_map -> constr -> types -> constr
 
 (** Conversion with inference of universe constraints *)
 val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f814028f9..7d2c96bb9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -743,7 +743,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let argloc = loc_of_glob_constr c in
 	let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in
         let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in
-        let resty = EConstr.of_constr resty in
       	  match EConstr.kind !evdref resty with
 	  | Prod (na,c1,c2) ->
 	    let tycon = Some c1 in
@@ -917,7 +916,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      @[EConstr.of_constr (build_dependent_constructor cs)] in
 	    let lp = lift cs.cs_nargs p in
 	    let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in
-	    let fty = EConstr.of_constr fty in
 	    let fj = pretype (mk_tycon fty) env_f evdref lvar d in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
@@ -1100,7 +1098,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
 	     let sigma =  !evdref in
 	     let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
 	     let t = EConstr.of_constr t in
-	       match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma t)) with
+	       match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with
                | Sort s -> s
                | Evar ev when is_Type (existential_type sigma ev) ->
 		   evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3230f92da..8362a2a26 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -324,15 +324,15 @@ let lookup_canonical_conversion (proj,pat) =
   assoc_pat pat (Refmap.find proj !object_table)
 
 let is_open_canonical_projection env sigma (c,args) =
+  let open EConstr in
   try
-    let c = EConstr.Unsafe.to_constr c in
-    let ref = global_of_constr c in
+    let (ref, _) = Termops.global_of_constr sigma c in
     let n = find_projection_nparams ref in
     (** Check if there is some canonical projection attached to this structure *)
     let _ = Refmap.find ref !object_table in
     try
       let arg = whd_all env sigma (Stack.nth args n) in
-      let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in
-      not (isConstruct hd)
+      let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
+      not (isConstruct sigma hd)
     with Failure _ -> false
   with Not_found -> false
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6ec3cd985..45e7abcb7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -588,10 +588,10 @@ end
 (** The type of (machine) states (= lambda-bar-calculus' cuts) *)
 type state = constr * constr Stack.t
 
-type contextual_reduction_function = env -> evar_map -> constr -> Constr.constr
+type contextual_reduction_function = env -> evar_map -> constr -> constr
 type reduction_function = contextual_reduction_function
-type local_reduction_function = evar_map -> constr -> Constr.constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (Constr.constr, 'r) Sigma.sigma }
+type local_reduction_function = evar_map -> constr -> constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
 
 type contextual_stack_reduction_function =
     env -> evar_map -> constr -> constr * constr list
@@ -629,19 +629,18 @@ let safe_meta_value sigma ev =
 
 let strong whdfun env sigma t =
   let rec strongrec env t =
-    let t = EConstr.of_constr (whdfun env sigma t) in
-    map_constr_with_full_binders sigma push_rel strongrec env t in
-  EConstr.Unsafe.to_constr (strongrec env t)
+    map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in
+  strongrec env t
 
 let local_strong whdfun sigma =
-  let rec strongrec t = EConstr.map sigma strongrec (EConstr.of_constr (whdfun sigma t)) in
-  fun c -> EConstr.Unsafe.to_constr (strongrec c)
+  let rec strongrec t = EConstr.map sigma strongrec (whdfun sigma t) in
+  strongrec
 
 let rec strong_prodspine redfun sigma c =
-  let x = EConstr.of_constr (redfun sigma c) in
+  let x = redfun sigma c in
   match EConstr.kind sigma x with
-    | Prod (na,a,b) -> EConstr.Unsafe.to_constr (mkProd (na,a,EConstr.of_constr (strong_prodspine redfun sigma b)))
-    | _ -> EConstr.Unsafe.to_constr x
+    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
+    | _ -> x
 
 (*************************************)
 (*** Reduction using bindingss ***)
@@ -1140,7 +1139,7 @@ let iterate_whd_gen refold flags env sigma s =
   in aux s
 
 let red_of_state_red f sigma x =
-  EConstr.Unsafe.to_constr (Stack.zip sigma (f sigma (x,Stack.empty)))
+  Stack.zip sigma (f sigma (x,Stack.empty))
 
 (* 0. No Reduction Functions *)
 
@@ -1217,9 +1216,9 @@ let nf_evar = Evarutil.nf_evar
 let clos_norm_flags flgs env sigma t =
   try
     let evars ev = safe_evar_value sigma ev in
-    CClosure.norm_val
+    EConstr.of_constr (CClosure.norm_val
       (CClosure.create_clos_infos ~evars flgs env)
-      (CClosure.inject (EConstr.Unsafe.to_constr t))
+      (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> error "Tried to normalize ill-typed term"
 
 let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
@@ -1309,6 +1308,7 @@ let sigma_univ_state =
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
+  (** FIXME *)
   let x = EConstr.Unsafe.to_constr x in
   let y = EConstr.Unsafe.to_constr y in
   try
@@ -1352,8 +1352,8 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
 (********************************************************************)
 
 let whd_meta sigma c = match EConstr.kind sigma c with
-  | Meta p -> (try meta_value sigma p with Not_found -> EConstr.Unsafe.to_constr c)
-  | _ -> EConstr.Unsafe.to_constr c
+  | Meta p -> (try EConstr.of_constr (meta_value sigma p) with Not_found -> c)
+  | _ -> c
 
 let default_plain_instance_ident = Id.of_string "H"
 
@@ -1431,26 +1431,26 @@ let instance sigma s c =
  * error message. *)
 
 let hnf_prod_app env sigma t n =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
-    | Prod (_,_,b) -> EConstr.Unsafe.to_constr (subst1 n b)
+  match EConstr.kind sigma (whd_all env sigma t) with
+    | Prod (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
 
 let hnf_prod_appvect env sigma t nl =
-  Array.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  Array.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl
 
 let hnf_prod_applist env sigma t nl =
-  List.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  List.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl
 
 let hnf_lam_app env sigma t n =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
-    | Lambda (_,_,b) -> EConstr.Unsafe.to_constr (subst1 n b)
+  match EConstr.kind sigma (whd_all env sigma t) with
+    | Lambda (_,_,b) -> subst1 n b
     | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
 
 let hnf_lam_appvect env sigma t nl =
-  Array.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  Array.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl
 
 let hnf_lam_applist env sigma t nl =
-  List.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+  List.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl
 
 let bind_assum (na, t) =
   (na, t)
@@ -1458,7 +1458,6 @@ let bind_assum (na, t) =
 let splay_prod env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    let t = EConstr.of_constr t in
     match EConstr.kind sigma t with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
@@ -1470,7 +1469,6 @@ let splay_prod env sigma =
 let splay_lam env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    let t = EConstr.of_constr t in
     match EConstr.kind sigma t with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
@@ -1482,7 +1480,7 @@ let splay_lam env sigma =
 let splay_prod_assum env sigma =
   let rec prodec_rec env l c =
     let t = whd_allnolet env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    match EConstr.kind sigma t with
     | Prod (x,t,c)  ->
 	prodec_rec (push_rel (local_assum (x,t)) env)
 	  (Context.Rel.add (local_assum (x,t)) l) c
@@ -1491,9 +1489,9 @@ let splay_prod_assum env sigma =
 	  (Context.Rel.add (local_def (x,b,t)) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> 
-      let t' = whd_all env sigma (EConstr.of_constr t) in
-	if Term.eq_constr t t' then l,t
-	else prodec_rec env l (EConstr.of_constr t')
+      let t' = whd_all env sigma t in
+	if EConstr.eq_constr sigma t t' then l,t
+	else prodec_rec env l t'
   in
   prodec_rec env Context.Rel.empty
 
@@ -1506,8 +1504,8 @@ let splay_arity env sigma c =
 let sort_of_arity env sigma c = snd (splay_arity env sigma c)
 
 let splay_prod_n env sigma n =
-  let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else
-    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with
+  let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
+    match EConstr.kind sigma (whd_all env sigma c) with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
@@ -1516,8 +1514,8 @@ let splay_prod_n env sigma n =
   decrec env n Context.Rel.empty
 
 let splay_lam_n env sigma n =
-  let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else
-    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with
+  let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
+    match EConstr.kind sigma (whd_all env sigma c) with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
@@ -1526,7 +1524,7 @@ let splay_lam_n env sigma n =
   decrec env n Context.Rel.empty
 
 let is_sort env sigma t =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+  match EConstr.kind sigma (whd_all env sigma t) with
   | Sort s -> true
   | _ -> false
 
@@ -1559,7 +1557,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
 let find_conclusion env sigma =
   let rec decrec env c =
     let t = whd_all env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    match EConstr.kind sigma t with
       | Prod (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
       | Lambda (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
       | t -> t
@@ -1579,7 +1577,7 @@ let meta_value evd mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
       let metas = Metamap.bind valrec b.freemetas in
-      EConstr.of_constr (instance evd metas (EConstr.of_constr b.rebus))
+      instance evd metas (EConstr.of_constr b.rebus)
     | None -> mkMeta mv
   in
   valrec mv
@@ -1589,7 +1587,7 @@ let meta_instance sigma b =
   if Metaset.is_empty fm then b.rebus
   else
     let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
-    EConstr.of_constr (instance sigma c_sigma b.rebus)
+    instance sigma c_sigma b.rebus
 
 let nf_meta sigma c =
   let c = EConstr.Unsafe.to_constr c in
@@ -1609,7 +1607,6 @@ let meta_reducible_instance evd b =
   let metas = Metaset.fold fold fm Metamap.empty in
   let rec irec u =
     let u = whd_betaiota Evd.empty u (** FIXME *) in
-    let u = EConstr.of_constr u in
     match EConstr.kind evd u with
     | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
 	let m = destMeta evd (strip_outer_cast evd c) in
@@ -1674,7 +1671,7 @@ let head_unfold_under_prod ts env sigma c =
 	  match EConstr.kind sigma h with
 	    | Const cst -> beta_app sigma (unfold cst, l)
 	    | _ -> c in
-  EConstr.Unsafe.to_constr (aux c)
+  aux c
 
 let betazetaevar_applist sigma n c l =
   let rec stacklam n env t stack =
@@ -1684,4 +1681,4 @@ let betazetaevar_applist sigma n c l =
     | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
     | Evar _, _ -> applist (substl env t, stack)
     | _ -> anomaly (Pp.str "Not enough lambda/let's") in
-  EConstr.Unsafe.to_constr (stacklam n [] c l)
+  stacklam n [] c l
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 3b3242537..add1d186b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open EConstr
 open Univ
 open Evd
 open Environ
@@ -38,7 +39,6 @@ val set_refolding_in_reduction : bool -> unit
     cst applied to params must convertible to term of the state applied to args
 *)
 module Cst_stack : sig
-  open EConstr
   type t
   val empty : t
   val add_param : constr -> t -> t
@@ -52,7 +52,6 @@ end
 
 
 module Stack : sig
-  open EConstr
   type 'a app_node
 
   val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
@@ -109,19 +108,19 @@ end
 
 (************************************************************************)
 
-type state = EConstr.t * EConstr.t Stack.t
+type state = constr * constr Stack.t
 
-type contextual_reduction_function = env -> evar_map -> EConstr.t -> constr
+type contextual_reduction_function = env -> evar_map -> constr -> constr
 type reduction_function = contextual_reduction_function
-type local_reduction_function = evar_map -> EConstr.t -> constr
+type local_reduction_function = evar_map -> constr -> constr
 
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> EConstr.t -> (constr, 'r) Sigma.sigma }
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
 
 type contextual_stack_reduction_function =
-    env -> evar_map -> EConstr.t -> EConstr.t * EConstr.t list
+    env -> evar_map -> constr -> constr * constr list
 type stack_reduction_function = contextual_stack_reduction_function
 type local_stack_reduction_function =
-    evar_map -> EConstr.t -> EConstr.t * EConstr.t list
+    evar_map -> constr -> constr * constr list
 
 type contextual_state_reduction_function =
     env -> evar_map -> state -> state
@@ -139,13 +138,13 @@ val strong_prodspine : local_reduction_function -> local_reduction_function
 val stack_reduction_of_reduction :
   'a reduction_function -> 'a state_reduction_function
 i*)
-val stacklam : (state -> 'a) -> EConstr.t list -> evar_map -> EConstr.t -> EConstr.t Stack.t -> 'a
+val stacklam : (state -> 'a) -> constr list -> evar_map -> constr -> constr Stack.t -> 'a
 
 val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool ->
   CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
 
 val iterate_whd_gen : bool -> CClosure.RedFlags.reds ->
-  Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
+  Environ.env -> Evd.evar_map -> constr -> constr
 
 (** {6 Generic Optimized Reduction Function using Closures } *)
 
@@ -156,11 +155,11 @@ val nf_beta : local_reduction_function
 val nf_betaiota : local_reduction_function
 val nf_betaiotazeta : local_reduction_function
 val nf_all : reduction_function
-val nf_evar : evar_map -> constr -> constr
+val nf_evar : evar_map -> Constr.constr -> Constr.constr
 
 (** Lazy strategy, weak head reduction *)
 
-val whd_evar :  evar_map -> constr -> constr
+val whd_evar :  evar_map -> Constr.constr -> Constr.constr
 val whd_nored : local_reduction_function
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
@@ -198,45 +197,45 @@ val whd_zeta_stack : local_stack_reduction_function
 val whd_zeta_state : local_state_reduction_function
 val whd_zeta : local_reduction_function
 
-val shrink_eta : EConstr.constr -> EConstr.constr
+val shrink_eta : constr -> constr
 
 (** Various reduction functions *)
 
-val safe_evar_value : evar_map -> existential -> constr option
+val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
 
-val beta_applist : evar_map -> EConstr.t * EConstr.t list -> EConstr.constr
+val beta_applist : evar_map -> constr * constr list -> constr
 
-val hnf_prod_app     : env ->  evar_map -> EConstr.t -> EConstr.t -> constr
-val hnf_prod_appvect : env ->  evar_map -> EConstr.t -> EConstr.t array -> constr
-val hnf_prod_applist : env ->  evar_map -> EConstr.t -> EConstr.t list -> constr
-val hnf_lam_app      : env ->  evar_map -> EConstr.t -> EConstr.t -> constr
-val hnf_lam_appvect  : env ->  evar_map -> EConstr.t -> EConstr.t array -> constr
-val hnf_lam_applist  : env ->  evar_map -> EConstr.t -> EConstr.t list -> constr
+val hnf_prod_app     : env ->  evar_map -> constr -> constr -> constr
+val hnf_prod_appvect : env ->  evar_map -> constr -> constr array -> constr
+val hnf_prod_applist : env ->  evar_map -> constr -> constr list -> constr
+val hnf_lam_app      : env ->  evar_map -> constr -> constr -> constr
+val hnf_lam_appvect  : env ->  evar_map -> constr -> constr array -> constr
+val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 
-val splay_prod : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr
-val splay_lam : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr
-val splay_arity : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * sorts
-val sort_of_arity : env -> evar_map -> EConstr.t -> sorts
-val splay_prod_n : env ->  evar_map -> int -> EConstr.t -> Context.Rel.t * constr
-val splay_lam_n : env ->  evar_map -> int -> EConstr.t -> Context.Rel.t * constr
+val splay_prod : env ->  evar_map -> constr -> (Name.t * constr) list * constr
+val splay_lam : env ->  evar_map -> constr -> (Name.t * constr) list * constr
+val splay_arity : env ->  evar_map -> constr -> (Name.t * constr) list * sorts
+val sort_of_arity : env -> evar_map -> constr -> sorts
+val splay_prod_n : env ->  evar_map -> int -> constr -> Context.Rel.t * constr
+val splay_lam_n : env ->  evar_map -> int -> constr -> Context.Rel.t * constr
 val splay_prod_assum :
-  env ->  evar_map -> EConstr.t -> Context.Rel.t * constr
+  env ->  evar_map -> constr -> Context.Rel.t * constr
 
 type 'a miota_args = {
-  mP      : EConstr.t;     (** the result type *)
-  mconstr : EConstr.t;     (** the constructor *)
+  mP      : constr;     (** the result type *)
+  mconstr : constr;     (** the constructor *)
   mci     : case_info;  (** special info to re-build pattern *)
   mcargs  : 'a list;    (** the constructor's arguments *)
   mlf     : 'a array }  (** the branch code vector *)
 
-val reducible_mind_case : evar_map -> EConstr.t -> bool
-val reduce_mind_case : evar_map -> EConstr.t miota_args -> EConstr.t
+val reducible_mind_case : evar_map -> constr -> bool
+val reduce_mind_case : evar_map -> constr miota_args -> constr
 
-val find_conclusion : env -> evar_map -> EConstr.t -> (EConstr.t,EConstr.t) kind_of_term
-val is_arity : env ->  evar_map -> EConstr.t -> bool
-val is_sort : env -> evar_map -> EConstr.types -> bool
+val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term
+val is_arity : env ->  evar_map -> constr -> bool
+val is_sort : env -> evar_map -> types -> bool
 
-val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> (EConstr.t, EConstr.t) pfixpoint -> EConstr.t
+val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixpoint -> constr
 val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
@@ -249,14 +248,14 @@ type conversion_test = constraints -> constraints
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
-val is_conv : ?reds:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool
-val is_conv_leq : ?reds:transparent_state -> env ->  evar_map -> EConstr.t -> EConstr.t -> bool
-val is_fconv : ?reds:transparent_state -> conv_pb -> env ->  evar_map -> EConstr.t -> EConstr.t -> bool
+val is_conv : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool
+val is_conv_leq : ?reds:transparent_state -> env ->  evar_map -> constr -> constr -> bool
+val is_fconv : ?reds:transparent_state -> conv_pb -> env ->  evar_map -> constr -> constr -> bool
 
 (** [check_conv] Checks universe constraints only.
     pb defaults to CUMUL and ts to a full transparent state.
  *)
-val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> EConstr.t -> EConstr.t -> bool
+val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> constr -> constr -> bool
 
 (** [infer_conv] Adds necessary universe constraints to the evar map.
     pb defaults to CUMUL and ts to a full transparent state.
@@ -264,29 +263,29 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> ECo
     otherwise returns false in that case.
  *)
 val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
-  env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool
+  env -> evar_map -> constr -> constr -> evar_map * bool
 
 (** Conversion with inference of universe constraints *)
-val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> EConstr.constr -> EConstr.constr ->
+val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
   evar_map * bool) -> unit
-val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> EConstr.constr -> EConstr.constr ->
+val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
   evar_map * bool
 
 
 (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
 conversion function. Used to pretype vm and native casts. *)
 val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
-    (constr, evar_map) Reduction.generic_conversion_function) ->
+    (Constr.constr, evar_map) Reduction.generic_conversion_function) ->
   ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
-  evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool
+  evar_map -> constr -> constr -> evar_map * bool
 
 (** {6 Special-Purpose Reduction Functions } *)
 
 val whd_meta : local_reduction_function
-val plain_instance : evar_map -> EConstr.t Metamap.t -> EConstr.t -> EConstr.t
-val instance : evar_map -> EConstr.t Metamap.t -> EConstr.t -> constr
+val plain_instance : evar_map -> constr Metamap.t -> constr -> constr
+val instance : evar_map -> constr Metamap.t -> constr -> constr
 val head_unfold_under_prod : transparent_state -> reduction_function
-val betazetaevar_applist : evar_map -> int -> EConstr.t -> EConstr.t list -> constr
+val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
 
 (** {6 Heuristic for Conversion with Evar } *)
 
@@ -295,6 +294,6 @@ val whd_betaiota_deltazeta_for_iota_state :
   state * Cst_stack.t
 
 (** {6 Meta-related reduction functions } *)
-val meta_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr
-val nf_meta       : evar_map -> EConstr.constr -> EConstr.constr
-val meta_reducible_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr
+val meta_instance : evar_map -> constr freelisted -> constr
+val nf_meta       : evar_map -> constr -> constr
+val meta_reducible_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3142ea5cb..7db30bf23 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -74,7 +74,7 @@ let get_type_from_constraints env sigma t =
 let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
-      match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma typ)) with
+      match EConstr.kind sigma (whd_all env sigma typ) with
         | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest
         | _ -> retype_error NonFunctionalConstruction
 
@@ -83,7 +83,7 @@ let rec subst_type env sigma typ = function
 
 let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env n ar args =
-    match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma ar)), args with
+    match EConstr.kind sigma (whd_all env sigma ar), args with
     | Prod (na, t, b), h::l -> concl_of_arity (push_rel (local_def (na, lift n h, t)) env) (n + 1) b l
     | Sort s, [] -> s
     | _ -> retype_error NotASort
@@ -94,7 +94,7 @@ let type_of_var env id =
   with Not_found -> retype_error (BadVariable id)
 
 let decomp_sort env sigma t =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+  match EConstr.kind sigma (whd_all env sigma t) with
   | Sort s -> s
   | _ -> retype_error NotASort
 
@@ -123,9 +123,9 @@ let retype ?(polyprop=true) sigma =
           with Not_found -> retype_error BadRecursiveType
         in
         let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
-        let t = EConstr.of_constr (betazetaevar_applist sigma n p realargs) in
-        (match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma (type_of env t))) with
-          | Prod _ -> EConstr.of_constr (whd_beta sigma (applist (t, [c])))
+        let t = betazetaevar_applist sigma n p realargs in
+        (match EConstr.kind sigma (whd_all env sigma (type_of env t)) with
+          | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)
     | Lambda (name,c1,c2) ->
           mkProd (name, c1, type_of (push_rel (local_assum (name,c1)) env) c2)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1d179c683..02524f896 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -425,7 +425,7 @@ let solve_arity_problem env sigma fxminargs c =
   let evm = ref sigma in
   let set_fix i = evm := Evd.define i (Constr.mkVar vfx) !evm in
   let rec check strict c =
-    let c' = EConstr.of_constr (whd_betaiotazeta sigma c) in
+    let c' = whd_betaiotazeta sigma c in
     let (h,rcargs) = decompose_app_vect sigma c' in
     match EConstr.kind sigma h with
         Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) ->
@@ -473,7 +473,7 @@ let reduce_fix whdfun sigma fix stack =
     | None -> NotReducible
     | Some (recargnum,recarg) ->
         let (recarg'hd,_ as recarg') = whdfun sigma recarg in
-        let stack' = List.assign stack recargnum (EConstr.applist recarg') in
+        let stack' = List.assign stack recargnum (applist recarg') in
 	(match EConstr.kind sigma recarg'hd with
            | Construct _ -> Reduced (contract_fix sigma fix, stack')
 	   | _ -> NotReducible)
@@ -483,7 +483,7 @@ let contract_fix_use_function env sigma f
   let nbodies = Array.length recindices in
   let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
   let lbodies = List.init nbodies make_Fi in
-  substl_checking_arity env (List.rev lbodies) sigma (EConstr.of_constr (nf_beta sigma bodies.(bodynum)))
+  substl_checking_arity env (List.rev lbodies) sigma (nf_beta sigma bodies.(bodynum))
 
 let reduce_fix_use_function env sigma f whfun fix stack =
   match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
@@ -495,7 +495,7 @@ let reduce_fix_use_function env sigma f whfun fix stack =
 	    (recarg, [])
 	  else
 	    whfun recarg in
-        let stack' = List.assign stack recargnum (EConstr.applist recarg') in
+        let stack' = List.assign stack recargnum (applist recarg') in
 	(match EConstr.kind sigma recarg'hd with
            | Construct _ ->
 	       Reduced (contract_fix_use_function env sigma f fix,stack')
@@ -507,7 +507,7 @@ let contract_cofix_use_function env sigma f
   let make_Fi j = (mkCoFix(j,typedbodies), f j) in
   let subbodies = List.init nbodies make_Fi in
   substl_checking_arity env (List.rev subbodies)
-    sigma (EConstr.of_constr (nf_beta sigma bodies.(bodynum)))
+    sigma (nf_beta sigma bodies.(bodynum))
 
 let reduce_mind_case_use_function func env sigma mia =
   match EConstr.kind sigma mia.mconstr with
@@ -689,7 +689,7 @@ let rec red_elim_const env sigma ref u largs =
 	let whfun = whd_construct_stack env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
 	   | NotReducible -> raise Redelimination
-           | Reduced (c,rest) -> (EConstr.of_constr (nf_beta sigma c), rest), nocase)
+           | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
     | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
 	let rec descend (ref,u) args =
 	  let c = reference_value env sigma ref u in
@@ -704,14 +704,14 @@ let rec red_elim_const env sigma ref u largs =
 	let whfun = whd_construct_stack env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
 	   | NotReducible -> raise Redelimination
-	   | Reduced (c,rest) -> (EConstr.of_constr (nf_beta sigma c), rest), nocase)
+	   | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
     | NotAnElimination when unfold_nonelim ->
          let c = reference_value env sigma ref u in
-           (EConstr.of_constr (whd_betaiotazeta sigma (applist (c, largs))), []), nocase
+           (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
     | _ -> raise Redelimination
     with Redelimination when unfold_anyway ->
        let c = reference_value env sigma ref u in
-	 (EConstr.of_constr (whd_betaiotazeta sigma (applist (c, largs))), []), nocase
+	 (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
 
 and reduce_params env sigma stack l =
   let len = List.length stack in
@@ -721,7 +721,7 @@ and reduce_params env sigma stack l =
 	let arg = List.nth stack i in
 	let rarg = whd_construct_stack env sigma arg in
 	  match EConstr.kind sigma (fst rarg) with
-	  | Construct _ -> List.assign stack i (EConstr.applist rarg)
+	  | Construct _ -> List.assign stack i (applist rarg)
 	  | _ -> raise Redelimination)
       stack l
     
@@ -817,9 +817,9 @@ and whd_construct_stack env sigma s =
 *)
 
 let try_red_product env sigma c =
-  let simpfun c = EConstr.of_constr (clos_norm_flags betaiotazeta env sigma c) in
+  let simpfun c = clos_norm_flags betaiotazeta env sigma c in
   let rec redrec env x =
-    let x = EConstr.of_constr (whd_betaiota sigma x) in
+    let x = whd_betaiota sigma x in
     match EConstr.kind sigma x with
       | App (f,l) ->
           (match EConstr.kind sigma f with
@@ -856,7 +856,7 @@ let try_red_product env sigma c =
 	     | None -> raise Redelimination
 	     | Some c -> c)
 	| _ -> raise Redelimination)
-  in EConstr.Unsafe.to_constr (redrec env c)
+  in redrec env c
 
 let red_product env sigma c =
   try try_red_product env sigma c
@@ -953,7 +953,7 @@ let hnf_constr = whd_simpl_orelse_delta_but_fix
 (* The "simpl" reduction tactic *)
 
 let whd_simpl env sigma c =
-  EConstr.Unsafe.to_constr (EConstr.applist (whd_simpl_stack env sigma c))
+  applist (whd_simpl_stack env sigma c)
 
 let simpl env sigma c = strong whd_simpl env sigma c
 
@@ -1010,7 +1010,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
         if locs != [] then
           ignore (traverse_below (Some (!pos-1)) envc t);
 	let Sigma (t, evm, _) = (f subst).e_redfun env (Sigma.Unsafe.of_evar_map !evd) t in
-	(evd := Sigma.to_evar_map evm; EConstr.of_constr t)
+	(evd := Sigma.to_evar_map evm; t)
       end
       else
 	traverse_below nested envc t
@@ -1029,7 +1029,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
   in
   let t' = traverse None (env,c) t in
   if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
-  Sigma.Unsafe.of_pair (EConstr.Unsafe.to_constr t', !evd)
+  Sigma.Unsafe.of_pair (t', !evd)
   end }
 
 let contextually byhead occs f env sigma t =
@@ -1080,7 +1080,7 @@ let string_of_evaluable_ref env = function
 
 let unfold env sigma name c =
   if is_evaluable env name then
-    EConstr.of_constr (clos_norm_flags (unfold_red name) env sigma c)
+    clos_norm_flags (unfold_red name) env sigma c
   else
     error (string_of_evaluable_ref env name^" is opaque.")
 
@@ -1098,7 +1098,7 @@ let unfoldoccs env sigma (occs,name) c =
     | [] -> ()
     | _ -> error_invalid_occurrence rest
     in
-    EConstr.of_constr (nf_betaiotazeta sigma uc)
+    nf_betaiotazeta sigma uc
   in
   match occs with
     | NoOccurrences -> c
@@ -1108,17 +1108,17 @@ let unfoldoccs env sigma (occs,name) c =
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c =
-  EConstr.Unsafe.to_constr (List.fold_left (fun c occname -> unfoldoccs env sigma occname c) c loccname)
+  List.fold_left (fun c occname -> unfoldoccs env sigma occname c) c loccname
 
 (* Re-folding constants tactics: refold com in term c *)
 let fold_one_com com env sigma c =
   let rcom =
-    try EConstr.of_constr (red_product env sigma com)
+    try red_product env sigma com
     with Redelimination -> error "Not reducible." in
   (* Reason first on the beta-iota-zeta normal form of the constant as
      unfold produces it, so that the "unfold f; fold f" configuration works
      to refold fix expressions *)
-  let a = subst_term sigma (EConstr.of_constr (clos_norm_flags unfold_side_red env sigma rcom)) c in
+  let a = subst_term sigma (clos_norm_flags unfold_side_red env sigma rcom) c in
   if not (EConstr.eq_constr sigma a c) then
     Vars.subst1 com a
   else
@@ -1128,12 +1128,12 @@ let fold_one_com com env sigma c =
     Vars.subst1 com a
 
 let fold_commands cl env sigma c =
-  EConstr.Unsafe.to_constr (List.fold_right (fun com c -> fold_one_com com env sigma c) (List.rev cl) c)
+  List.fold_right (fun com c -> fold_one_com com env sigma c) (List.rev cl) c
 
 
 (* call by value reduction functions *)
 let cbv_norm_flags flags env sigma t =
-  cbv_norm (create_cbv_infos flags env sigma) t
+  EConstr.of_constr (cbv_norm (create_cbv_infos flags env sigma) t)
 
 let cbv_beta = cbv_norm_flags beta empty_env
 let cbv_betaiota = cbv_norm_flags betaiota empty_env
@@ -1163,7 +1163,7 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
   let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in
   try
     let _ = Typing.unsafe_type_of env sigma abstr_trm in
-    Sigma.Unsafe.of_pair (EConstr.Unsafe.to_constr (applist(abstr_trm, List.map snd loccs_trm)), sigma)
+    Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
   end }
@@ -1189,7 +1189,6 @@ let check_not_primitive_record env ind =
 let reduce_to_ind_gen allow_product env sigma t =
   let rec elimrec env t l =
     let t = hnf_constr env sigma t in
-    let t = EConstr.of_constr t in
     match EConstr.kind sigma (fst (decompose_app_vect sigma t)) with
       | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l)
       | Prod (n,ty,t') ->
@@ -1202,7 +1201,6 @@ let reduce_to_ind_gen allow_product env sigma t =
 	  (* Last chance: we allow to bypass the Opaque flag (as it
 	     was partially the case between V5.10 and V8.1 *)
 	  let t' = whd_all env sigma t in
-	  let t' = EConstr.of_constr t' in
 	  match EConstr.kind sigma (fst (decompose_app_vect sigma t')) with
 	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
 	    | _ -> user_err  (str"Not an inductive product.")
@@ -1285,7 +1283,6 @@ let reduce_to_ref_gen allow_product env sigma ref t =
 	  with Not_found ->
           try
 	    let t' = nf_betaiota sigma (one_step_reduce env sigma t) in
-	    let t' = EConstr.of_constr t' in
             elimrec env t' l
           with NotStepReducible -> error_cannot_recognize ref
   in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index f59a6dcd9..9ee34341b 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -291,6 +291,7 @@ let build_subclasses ~check env sigma glob pri =
 	let instapp = 
 	  Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect 0 rels)))
 	in
+	let instapp = EConstr.Unsafe.to_constr instapp in
 	let projargs = Array.of_list (args @ [instapp]) in
 	let projs = List.map_filter 
 	  (fun (n, b, proj) ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 40ef2450a..f67e0bddc 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -53,7 +53,7 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl =
   EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
 
 let e_type_judgment env evdref j =
-  match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref j.uj_type)) with
+  match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
@@ -71,7 +71,7 @@ let e_judge_of_apply env evdref funj argjv =
       { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
         uj_type = typ }
   | hj::restjl ->
-      match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
+      match EConstr.kind !evdref (whd_all env !evdref typ) with
       | Prod (_,c1,c2) ->
 	 if Evarconv.e_cumul env evdref hj.uj_type c1 then
 	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
@@ -104,7 +104,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
   let allowed_sorts = elim_sorts specif in
   let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
   let rec srec env pt ar =
-    let pt' = EConstr.of_constr (whd_all env !evdref pt) in
+    let pt' = whd_all env !evdref pt in
     match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
         if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
@@ -144,7 +144,6 @@ let e_type_case_branches env evdref (ind,largs) pj c =
   let lc = Array.map EConstr.of_constr lc in
   let n = (snd specif).Declarations.mind_nrealdecls in
   let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
-  let ty = EConstr.of_constr ty in
   (lc, ty)
 
 let e_judge_of_case env evdref ci pj cj lfj =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 169dd45bc..8a8649f11 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -75,7 +75,6 @@ let occur_meta_evd sigma mv c =
   let rec occrec c =
     (* Note: evars are not instantiated by terms with metas *)
     let c = whd_meta sigma c in
-    let c = EConstr.of_constr c in
     match EConstr.kind sigma c with
     | Meta mv' when Int.equal mv mv' -> raise Occur
     | _ -> EConstr.iter sigma occrec c
@@ -1003,24 +1002,24 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	    (match expand_key flags.modulo_delta curenv sigma cf1 with
 	    | Some c ->
 		unirec_rec curenvnb pb opt substn
-                  (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l1)))) cN
+                  (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 	    | None ->
 		(match expand_key flags.modulo_delta curenv sigma cf2 with
 		| Some c ->
 		    unirec_rec curenvnb pb opt substn cM
-                      (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l2))))
+                      (whd_betaiotazeta sigma (mkApp(c,l2)))
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
 	| Some false ->
 	    (match expand_key flags.modulo_delta curenv sigma cf2 with
 	    | Some c ->
 		unirec_rec curenvnb pb opt substn cM
-                  (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l2))))
+                  (whd_betaiotazeta sigma (mkApp(c,l2)))
 	    | None ->
 		(match expand_key flags.modulo_delta curenv sigma cf1 with
 		| Some c ->
 		    unirec_rec curenvnb pb opt substn
-                      (EConstr.of_constr (whd_betaiotazeta sigma (mkApp(c,l1)))) cN
+                      (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
 
@@ -1233,7 +1232,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
       Sigma (c, evd, p)
     else
       let sigma = Sigma.to_evar_map evd in
-      match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma cty)) with
+      match EConstr.kind sigma (whd_all env sigma cty) with
       | Prod (_,c1,c2) ->
         let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
@@ -1263,7 +1262,7 @@ let w_coerce_to_type env evd c cty mvty =
        but there are cases where it though it was not rigid (like in
        fst (nat,nat)) and stops while it could have seen that it is rigid *)
     let cty = Tacred.hnf_constr env evd cty in
-      try_to_coerce env evd c (EConstr.of_constr cty) tycon
+      try_to_coerce env evd c cty tycon
 	  
 let w_coerce env evd mv c =
   let cty = get_type_of env evd c in
@@ -1276,7 +1275,6 @@ let unify_to_type env sigma flags c status u =
   let t = get_type_of env sigma (nf_meta sigma c) in
   let t = EConstr.of_constr t in
   let t = nf_betaiota sigma (nf_meta sigma t) in
-  let t = EConstr.of_constr t in
     unify_0 env sigma CUMUL flags t u
 
 let unify_type env sigma flags mv status c =
@@ -1379,7 +1377,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
     	  else
             let evd' =
               if occur_meta_evd evd mv c then
-                if isMetaOf mv (whd_all env evd c) then evd
+                if isMetaOf evd mv (whd_all env evd c) then evd
                 else error_cannot_unify env evd (mkMeta mv,c)
               else
 	        meta_assign mv (EConstr.Unsafe.to_constr c,(status,TypeProcessed)) evd in
@@ -1618,7 +1616,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   (fun test -> match test.testing_state with
   | None -> None
   | Some (sigma,_,l) ->
-     let c = applist (EConstr.of_constr (nf_evar sigma (local_strong whd_meta sigma c)), l) in
+     let c = applist (EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr (local_strong whd_meta sigma c))), l) in
      let univs, subst = nf_univ_variables sigma in
      Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
 
@@ -1877,7 +1875,6 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
   List.fold_right
     (fun op (evd,l) ->
       let op = whd_meta evd op in
-      let op = EConstr.of_constr op in
       if isMeta evd op then
 	if flags.allow_K_in_toplevel_higher_order_unification then (evd,op::l)
 	else error_abstraction_over_meta env evd hdmeta (destMeta evd op)
@@ -1983,8 +1980,8 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
    convertible and first-order otherwise. But if failed if e.g. the type of
    Meta(1) had meta-variables in it. *)
 let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
-  let hd1,l1 = decompose_app_vect evd (EConstr.of_constr (whd_nored evd ty1)) in
-  let hd2,l2 = decompose_app_vect evd (EConstr.of_constr (whd_nored evd ty2)) in
+  let hd1,l1 = decompose_app_vect evd (whd_nored evd ty1) in
+  let hd2,l2 = decompose_app_vect evd (whd_nored evd ty2) in
   let is_empty1 = Array.is_empty l1 in
   let is_empty2 = Array.is_empty l2 in
     match EConstr.kind evd hd1, not is_empty1, EConstr.kind evd hd2, not is_empty2 with
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 31693d82f..74998349b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -360,7 +360,7 @@ let cbv_vm env sigma c t  =
   let c = EConstr.to_constr sigma c in
   let t = EConstr.to_constr sigma t in
   let v = Vconv.val_of_constr env c in
-  nf_val env sigma v t
+  EConstr.of_constr (nf_val env sigma v t)
 
 let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
   Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb)
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 650f3f291..8a4202c88 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -10,4 +10,4 @@ open EConstr
 open Environ
 
 (** {6 Reduction functions } *)
-val cbv_vm : env -> Evd.evar_map -> constr -> types -> Constr.t
+val cbv_vm : env -> Evd.evar_map -> constr -> types -> constr
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index ab0ce7e56..e66d3aafe 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -73,7 +73,8 @@ let print_ref reduce ref =
   let typ = Global.type_of_global_unsafe ref in
   let typ =
     if reduce then
-      let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ)
+      let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) in
+      let ccl = EConstr.Unsafe.to_constr ccl
       in it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
@@ -595,6 +596,7 @@ let gallina_print_context with_values =
 
 let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} =
   let ntrm = red_fun env sigma (EConstr.of_constr trm) in
+  let ntrm = EConstr.Unsafe.to_constr ntrm in
   (str "     = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ))
 
 (******************************************)
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 572db1d40..a428ab0ed 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -60,7 +60,7 @@ let refresh_undefined_univs clenv =
       { clenv with evd = evd'; templval = map_freelisted clenv.templval;
 	templtyp = map_freelisted clenv.templtyp }, subst
 
-let clenv_hnf_constr ce t = EConstr.of_constr (hnf_constr (cl_env ce) (cl_sigma ce) t)
+let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
 let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c)
 
@@ -71,7 +71,6 @@ let mk_freelisted c =
 
 let clenv_push_prod cl =
   let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
-  let typ = EConstr.of_constr typ in
   let rec clrec typ = match EConstr.kind cl.evd typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
@@ -266,7 +265,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus)))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
@@ -480,7 +479,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u)))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -498,7 +497,6 @@ let clenv_unify_binding_type clenv c t u =
 let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
-  let c_typ = EConstr.of_constr c_typ in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
   let c = EConstr.Unsafe.to_constr c in
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 829c96296..98ad9ebe3 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -34,7 +34,7 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
-  | MetaInType of constr
+  | MetaInType of EConstr.constr
 
   (* Errors raised by the tactics *)
   | IntroNeedsProduct
@@ -347,10 +347,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       match kind_of_term trm with
       | Meta _ ->
 	let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
-	  if !check && occur_meta sigma (EConstr.of_constr conclty) then
+	  if !check && occur_meta sigma conclty then
 	    raise (RefinerError (MetaInType conclty));
-	  let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr conclty) in
+	  let (gl,ev,sigma) = mk_goal hyps conclty in
 	  let ev = EConstr.Unsafe.to_constr ev in
+	  let conclty = EConstr.Unsafe.to_constr conclty in
 	  gl::goalacc, conclty, sigma, ev
 
       | Cast (t,k, ty) ->
@@ -425,7 +426,7 @@ and mk_hdgoals sigma goal goalacc trm =
   match kind_of_term trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-	let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr ty))) in
+	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in
 	let ev = EConstr.Unsafe.to_constr ev in
 	gl::goalacc,ty,sigma,ev
 
@@ -474,6 +475,7 @@ and mk_hdgoals sigma goal goalacc trm =
 and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
     let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in
+    let t = EConstr.Unsafe.to_constr t in
     let rec collapse t = match kind_of_term t with
     | LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
     | _ -> t
@@ -537,7 +539,7 @@ let prim_refiner r sigma goal =
     (* Logical rules *)
     | Cut (b,replace,id,t) ->
 (*        if !check && not (Retyping.get_sort_of env sigma t) then*)
-        let (sg1,ev1,sigma) = mk_goal sign (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr t))) in
+        let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in
 	let sign,t,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 8c8a01cad..5fe28ac76 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -43,7 +43,7 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
-  | MetaInType of constr
+  | MetaInType of EConstr.constr
 
   (*i Errors raised by the tactics i*)
   | IntroNeedsProduct
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index d4a58da32..a830e25d9 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -44,7 +44,7 @@ let whd_cbn flags env sigma t =
   let (state,_) =
     (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
   in
-  EConstr.Unsafe.to_constr (Reductionops.Stack.zip ~refold:true sigma state)
+  Reductionops.Stack.zip ~refold:true sigma state
 
 let strong_cbn flags =
   strong (whd_cbn flags)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index f3f19e854..7ecf0a9e8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -23,8 +23,6 @@ open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
-let compute env sigma c = EConstr.of_constr (compute env sigma c)
-
 let re_sig it  gc = { it = it; sigma = gc; }
 
 (**************************************************************)
@@ -229,13 +227,13 @@ module New = struct
   let pf_reduce_to_quantified_ind gl t =
     pf_apply reduce_to_quantified_ind gl t
 
-  let pf_hnf_constr gl t = EConstr.of_constr (pf_apply hnf_constr gl t)
+  let pf_hnf_constr gl t = pf_apply hnf_constr gl t
   let pf_hnf_type_of gl t =
-    EConstr.of_constr (pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)))
+    pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t))
 
   let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
 
-  let pf_whd_all gl t = EConstr.of_constr (pf_apply whd_all gl t)
+  let pf_whd_all gl t = pf_apply whd_all gl t
   let pf_compute gl t = pf_apply compute gl t
 
   let pf_nf_evar gl t = nf_evar (project gl) t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 7b387ac9a..21511b6f9 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -42,7 +42,7 @@ val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
 val pf_unsafe_type_of            : goal sigma -> EConstr.constr -> types
 val pf_type_of            : goal sigma -> EConstr.constr -> evar_map * types
-val pf_hnf_type_of        : goal sigma -> EConstr.constr -> types
+val pf_hnf_type_of        : goal sigma -> EConstr.constr -> EConstr.types
 
 val pf_get_hyp            : goal sigma -> Id.t -> Context.Named.Declaration.t
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
@@ -50,7 +50,7 @@ val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
 val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
 
-val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * constr
+val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * EConstr.constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
@@ -63,15 +63,15 @@ val pf_e_reduce :
   (env -> evar_map -> constr -> evar_map * constr) ->
   goal sigma -> constr -> evar_map * constr
 
-val pf_whd_all       : goal sigma -> EConstr.constr -> constr
-val pf_hnf_constr              : goal sigma -> EConstr.constr -> constr
-val pf_nf                      : goal sigma -> EConstr.constr -> constr
-val pf_nf_betaiota             : goal sigma -> EConstr.constr -> constr
+val pf_whd_all       : goal sigma -> EConstr.constr -> EConstr.constr
+val pf_hnf_constr              : goal sigma -> EConstr.constr -> EConstr.constr
+val pf_nf                      : goal sigma -> EConstr.constr -> EConstr.constr
+val pf_nf_betaiota             : goal sigma -> EConstr.constr -> EConstr.constr
 val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types
 val pf_reduce_to_atomic_ind     : goal sigma -> EConstr.types -> pinductive * EConstr.types
 val pf_compute                 : goal sigma -> EConstr.constr -> EConstr.constr
 val pf_unfoldn    : (occurrences * evaluable_global_reference) list
-  -> goal sigma -> EConstr.constr -> constr
+  -> goal sigma -> EConstr.constr -> EConstr.constr
 
 val pf_const_value : goal sigma -> pconstant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index d656206d6..029384297 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -285,6 +285,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
     | Some c -> Some c
     | None ->
 	let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *)
+	let t' = EConstr.Unsafe.to_constr t' in
 	match find_rel (it_mkProd_or_LetIn t' ctx) with
 	| Some c -> Some c
 	| None -> None
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index bf4e53b10..3a5347bbf 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -535,7 +535,6 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
       | _ ->
           let env' = Environ.push_rel_context ctx env in
           let ty' = Reductionops.whd_all env' sigma ar in
-          let ty' = EConstr.of_constr ty' in
                if not (EConstr.eq_constr sigma ty' ar) then iscl env' ty'
                else false
   in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 2d5c28eba..afc7e1547 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -69,7 +69,6 @@ let contradiction_context =
           let typ = nf_evar sigma (NamedDecl.get_type d) in
           let typ = EConstr.of_constr typ in
 	  let typ = whd_all env sigma typ in
-          let typ = EConstr.of_constr typ in
 	  if is_empty_type sigma typ then
 	    simplest_elim (mkVar id)
 	  else match EConstr.kind sigma typ with
@@ -106,7 +105,7 @@ let contradiction_context =
   end }
 
 let is_negation_of env sigma typ t =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+  match EConstr.kind sigma (whd_all env sigma t) with
     | Prod (na,t,u) ->
       is_empty_type sigma u && is_conv_leq env sigma typ t
     | _ -> false
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 57400d334..92e59c5ce 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -481,7 +481,7 @@ let unfold_head env sigma (ids, csts) c =
 	true, EConstr.of_constr (Environ.constant_value_in env c)
     | App (f, args) ->
 	(match aux f with
-	| true, f' -> true, EConstr.of_constr (Reductionops.whd_betaiota sigma (mkApp (f', args)))
+	| true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args))
 	| false, _ -> 
 	    let done_, args' = 
 	      Array.fold_left_i (fun i (done_, acc) arg -> 
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 57bac25b9..a8ea7446f 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -605,9 +605,9 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
         (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p)
 	  (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
 	    (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
-	      (Reductionops.whd_beta Evd.empty
+	      (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty
 		(EConstr.of_constr (applist (c,
-	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))))
+	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
       in c', ctx'
   | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 209c9eb66..494f36d7d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -413,7 +413,7 @@ 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 evd (EConstr.of_constr (whd_zeta evd hdcncl)) in
+  let isatomic = isProd evd (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 c type_of_cls in
@@ -453,7 +453,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let env = Proofview.Goal.env gl in
     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
+    let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in
       match match_with_equality_type sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -470,7 +470,6 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
                   Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
 	          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 lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -1051,7 +1050,7 @@ let onNegatedEquality with_evars tac =
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    match EConstr.kind sigma (EConstr.of_constr (hnf_constr env sigma ccl)) with
+    match EConstr.kind sigma (hnf_constr env sigma ccl) with
     | Prod (_,t,u) when is_empty_type sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
@@ -1133,7 +1132,6 @@ let make_tuple env sigma (rterm,rty) lind =
 let minimal_free_rels env sigma (c,cty) =
   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)
@@ -1380,7 +1378,6 @@ let inject_if_homogenous_dependent_pair ty =
 
 let simplify_args env sigma t =
   (* Quick hack to reduce in arguments of eq only *)
-  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])
@@ -1591,7 +1588,6 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   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 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 expected_goal in
   let sigma, _ = Typing.type_of env sigma body in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2b310033c..231695c35 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -768,7 +768,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	    code = with_uid (Give_exact (c, cty, ctx)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
-  let cty = if hnf then EConstr.of_constr (hnf_constr env sigma cty) else cty in
+  let cty = if hnf then hnf_constr env sigma cty else cty in
     match EConstr.kind sigma cty with
     | Prod _ ->
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
@@ -921,7 +921,6 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
   let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
-  let t = EConstr.of_constr t in
   let hd = head_constr sigma t in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 609fa1be8..ef3bfc9d0 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -125,7 +125,7 @@ let max_prefix_sign lid sign =
     | id::l -> snd (max_rec (id, sign_prefix id sign) l)
 *)
 let rec add_prods_sign env sigma t =
-  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+  match EConstr.kind sigma (whd_all env sigma t) with
     | Prod (na,c1,b) ->
 	let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
 	let b'= subst1 (mkVar id) b in
@@ -180,7 +180,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       (pty,goal)
   in
   let npty = nf_all env sigma pty in
-  let extenv = push_named (LocalAssum (p,npty)) env in
+  let extenv = push_named (nlocal_assum (p,npty)) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index dabe78b34..5ee29c089 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -582,7 +582,6 @@ let fix ido n = match ido with
 
 let rec check_is_mutcoind env sigma cl =
   let b = whd_all env sigma cl in
-  let b = EConstr.of_constr b in
   match EConstr.kind sigma b with
   | Prod (na, c1, b) ->
     check_is_mutcoind (push_rel (local_assum (na,c1)) env) sigma b
@@ -634,11 +633,11 @@ let cofix ido = match ido with
 (*          Reduction and conversion tactics                  *)
 (**************************************************************)
 
-type tactic_reduction = env -> evar_map -> constr -> Constr.constr
+type tactic_reduction = env -> evar_map -> constr -> constr
 
 let pf_reduce_decl redfun where decl gl =
   let open Context.Named.Declaration in
-  let redfun' c = EConstr.of_constr (Tacmach.New.pf_apply redfun gl c) in
+  let redfun' c = Tacmach.New.pf_apply redfun gl c in
   match decl with
   | LocalAssum (id,ty) ->
       let ty = EConstr.of_constr ty in
@@ -722,7 +721,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
 
 let reduct_in_concl (redfun,sty) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-    convert_concl_no_check (EConstr.of_constr (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl))) sty
+    convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
   end }
 
 let reduct_in_hyp ?(check=false) redfun (id,where) =
@@ -742,23 +741,25 @@ let reduct_option ?(check=false) redfun = function
 let pf_e_reduce_decl redfun where decl gl =
   let open Context.Named.Declaration in
   let sigma = Proofview.Goal.sigma gl in
-  let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (EConstr.of_constr c) in
+  let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma c in
   match decl with
   | LocalAssum (id,ty) ->
+      let ty = EConstr.of_constr ty in
       if where == InHypValueOnly then
 	user_err  (pr_id id ++ str " has no value.");
     let Sigma (ty', sigma, p) = redfun sigma ty in
-    Sigma (LocalAssum (id, ty'), sigma, p)
+    Sigma (nlocal_assum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
+      let b = EConstr.of_constr b in
+      let ty = EConstr.of_constr ty in
       let Sigma (b', sigma, p) = if where != InHypTypeOnly then redfun sigma b else Sigma.here b sigma in
       let Sigma (ty', sigma, q) = if where != InHypValueOnly then redfun sigma ty else Sigma.here ty sigma in
-      Sigma (LocalDef (id, b', ty'), sigma, p +> q)
+      Sigma (nlocal_def (id, b', ty'), sigma, p +> q)
 
 let e_reduct_in_concl ~check (redfun, sty) =
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
-    let c' = EConstr.of_constr c' in
     Sigma (convert_concl ~check c' sty, sigma, p)
   end }
 
@@ -779,7 +780,6 @@ let e_change_in_concl (redfun,sty) =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in
-    let c = EConstr.of_constr c in
     Sigma (convert_concl_no_check c sty, sigma, p)
   end }
 
@@ -787,18 +787,21 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
   let open Context.Named.Declaration in
   match decl with
   | LocalAssum (id,ty) ->
+      let ty = EConstr.of_constr ty in
       if where == InHypValueOnly then
 	user_err  (pr_id id ++ str " has no value.");
-    let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma (EConstr.of_constr ty) in
-    Sigma (LocalAssum (id, ty'), sigma, p)
+    let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in
+    Sigma (nlocal_assum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
+      let b = EConstr.of_constr b in
+      let ty = EConstr.of_constr ty in
       let Sigma (b', sigma, p) =
-	if where != InHypTypeOnly then (redfun true).e_redfun env sigma (EConstr.of_constr b) else Sigma.here b sigma
+	if where != InHypTypeOnly then (redfun true).e_redfun env sigma b else Sigma.here b sigma
       in
       let Sigma (ty', sigma, q) =
-	if where != InHypValueOnly then (redfun false).e_redfun env sigma (EConstr.of_constr ty) else Sigma.here ty sigma
+	if where != InHypValueOnly then (redfun false).e_redfun env sigma ty else Sigma.here ty sigma
       in
-      Sigma (LocalDef (id,b',ty'), sigma, p +> q)
+      Sigma (nlocal_def (id,b',ty'), sigma, p +> q)
 
 let e_change_in_hyp redfun (id,where) =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -818,21 +821,22 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
   let t1 = EConstr.of_constr t1 in
   if deep then begin
     let t2 = Retyping.get_type_of env sigma origc in
+    let t2 = EConstr.of_constr t2 in
     let sigma, t2 = Evarsolve.refresh_universes
-		      ~onlyalg:true (Some false) env sigma (EConstr.of_constr t2) in
+		      ~onlyalg:true (Some false) env sigma t2 in
     let t2 = EConstr.of_constr t2 in
     let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
     if not b then
       if
-        isSort sigma (EConstr.of_constr (whd_all env sigma t1)) &&
-        isSort sigma (EConstr.of_constr (whd_all env sigma t2))
+        isSort sigma (whd_all env sigma t1) &&
+        isSort sigma (whd_all env sigma t2)
       then (mayneedglobalcheck := true; sigma)
       else
         user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.")
     else sigma
   end
   else
-    if not (isSort sigma (EConstr.of_constr (whd_all env sigma t1))) then
+    if not (isSort sigma (whd_all env sigma t1)) then
       user_err ~hdr:"convert-check-hyp" (str "Not a type.")
     else sigma
 
@@ -843,7 +847,7 @@ let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun en
   let sigma = check_types env sigma mayneedglobalcheck deep t' c in
   let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
   if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
-  Sigma.Unsafe.of_pair (EConstr.Unsafe.to_constr t', sigma)
+  Sigma.Unsafe.of_pair (t', sigma)
 end }
 
 (* Use cumulativity only if changing the conclusion not a subterm *)
@@ -858,7 +862,7 @@ let change_on_subterm cv_pb deep t where = { e_redfun = begin fun env sigma c ->
         env sigma c in
   if !mayneedglobalcheck then
     begin
-      try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c))
+      try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) c)
       with e when catchable_exception e ->
         error "Replacement would lead to an ill-typed term."
     end;
@@ -1101,8 +1105,8 @@ let intros_replacing ids =
 (* User-level introduction tactics *)
 
 let lookup_hypothesis_as_renamed env ccl = function
-  | AnonHyp n -> Detyping.lookup_index_as_renamed env ccl n
-  | NamedHyp id -> Detyping.lookup_name_as_displayed env ccl id
+  | AnonHyp n -> Detyping.lookup_index_as_renamed env (EConstr.Unsafe.to_constr ccl) n
+  | NamedHyp id -> Detyping.lookup_name_as_displayed env (EConstr.Unsafe.to_constr ccl) id
 
 let lookup_hypothesis_as_renamed_gen red h gl =
   let env = Proofview.Goal.env gl in
@@ -1110,11 +1114,11 @@ let lookup_hypothesis_as_renamed_gen red h gl =
     match lookup_hypothesis_as_renamed env ccl h with
       | None when red ->
         let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in
-        let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) (EConstr.of_constr ccl) in
+        let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) ccl in
         aux c
       | x -> x
   in
-  try aux (EConstr.to_constr (Tacmach.New.project gl) (Proofview.Goal.concl gl))
+  try aux (Proofview.Goal.concl gl)
   with Redelimination -> None
 
 let is_quantified_hypothesis id gl =
@@ -1261,7 +1265,6 @@ let cut c =
         let typ = Typing.unsafe_type_of env sigma c in
         let typ = EConstr.of_constr typ in
         let typ = whd_all env sigma typ in
-        let typ = EConstr.of_constr typ in
         match EConstr.kind sigma typ with
         | Sort _ -> true
         | _ -> false
@@ -1270,7 +1273,7 @@ let cut c =
     if is_sort then
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
       (** Backward compat: normalize [c]. *)
-      let c = if normalize_cut then EConstr.of_constr (local_strong whd_betaiota sigma c) else c in
+      let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
       Refine.refine ~unsafe:true { run = begin fun h ->
         let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
         let Sigma (x, h, q) = Evarutil.new_evar env h c in
@@ -1755,7 +1758,6 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind :
     let thm_ty0 = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma c)) in
     let try_apply thm_ty nprod =
       try
-        let thm_ty = EConstr.of_constr thm_ty in
         let n = nb_prod_modulo_zeta sigma thm_ty - nprod in
         if n<0 then error "Applied theorem has not enough premisses.";
         let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
@@ -1766,7 +1768,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind :
     let rec try_red_apply thm_ty (exn0, info) =
       try
         (* Try to head-reduce the conclusion of the theorem *)
-        let red_thm = try_red_product env sigma (EConstr.of_constr thm_ty) in
+        let red_thm = try_red_product env sigma thm_ty in
         tclORELSEOPT
           (try_apply red_thm concl_nprod)
           (function (e, info) -> match e with
@@ -1880,7 +1882,6 @@ let progress_with_clause flags innerclause clause =
 
 let apply_in_once_main flags innerclause env sigma (d,lbind) =
   let thm = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma d)) in
-  let thm = EConstr.of_constr thm in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with e when CErrors.noncritical e ->
@@ -2183,7 +2184,6 @@ let apply_type newcl args =
     let store = Proofview.Goal.extra gl in
     Refine.refine { run = begin fun sigma ->
       let newcl = nf_betaiota (Sigma.to_evar_map sigma) newcl (* As in former Logic.refine *) in
-      let newcl = EConstr.of_constr newcl in
       let Sigma (ev, sigma, p) =
         Evarutil.new_evar env sigma ~principal:true ~store newcl in
       Sigma (applist (ev, args), sigma, p)
@@ -2377,7 +2377,6 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let whd_all = Tacmach.New.pf_apply whd_all gl in
     let t = whd_all (EConstr.of_constr (type_of (mkVar id))) in
-    let t = EConstr.of_constr t in
     let eqtac, thin = match match_with_equality_type sigma t with
     | Some (hdcncl,[_;lhs;rhs]) ->
         if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then
@@ -3039,7 +3038,7 @@ let unfold_body x =
   let xval = EConstr.of_constr xval in
   Tacticals.New.afterHyp x begin fun aft ->
   let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in
-  let rfun _ _ c = EConstr.Unsafe.to_constr (replace_vars [x, xval] c) in
+  let rfun _ _ c = replace_vars [x, xval] c in
   let reducth h = reduct_in_hyp rfun h in
   let reductc = reduct_in_concl (rfun, DEFAULTcast) in
   Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]
@@ -3692,7 +3691,6 @@ let abstract_args gl generalize_vars dep id defined f args =
   let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg =
     let name, ty, arity =
       let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
-      let c = EConstr.of_constr c in
       let decl = List.hd rel in
       RelDecl.get_name decl, RelDecl.get_type decl, c
     in
@@ -3855,9 +3853,7 @@ let specialize_eqs id gl =
   let acc' = it_mkLambda_or_LetIn acc ctx'' in
   let ty' = Tacred.whd_simpl env !evars ty'
   and acc' = Tacred.whd_simpl env !evars acc' in
-  let acc' = EConstr.of_constr acc' in
-  let ty' = Evarutil.nf_evar !evars ty' in
-  let ty' = EConstr.of_constr ty' in
+  let ty' = EConstr.of_constr (Evarutil.nf_evar !evars (EConstr.Unsafe.to_constr ty')) in
     if worked then
       tclTHENFIRST (Tacmach.internal_cut true id ty')
 	(Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl
@@ -4368,7 +4364,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
       let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in
       Sigma.Unsafe.of_pair (c, sigma)
     with e when catchable_exception e ->
-    try find_clause (EConstr.of_constr (try_red_product env sigma typ))
+    try find_clause (try_red_product env sigma typ)
     with Redelimination -> raise e in
   find_clause typ
 
@@ -4390,7 +4386,7 @@ let check_enough_applied env sigma elim =
   | None ->
       (* No eliminator given *)
       fun u ->
-      let t,_ = decompose_app sigma (EConstr.of_constr (whd_all env sigma u)) in isInd sigma t
+      let t,_ = decompose_app sigma (whd_all env sigma u) in isInd sigma t
   | Some elimc ->
       let elimt = Retyping.get_type_of env sigma (fst elimc) in
       let elimt = EConstr.of_constr elimt in
@@ -4716,7 +4712,7 @@ let maybe_betadeltaiota_concl allowred gl =
   if not allowred then concl
   else
     let env = Proofview.Goal.env gl in
-    EConstr.of_constr (whd_all env sigma concl)
+    whd_all env sigma concl
 
 let reflexivity_red allowred =
   Proofview.Goal.enter { enter = begin fun gl ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 630c660a1..b0d9dcb1c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -129,7 +129,7 @@ val exact_proof      : Constrexpr.constr_expr -> unit Proofview.tactic
 
 (** {6 Reduction tactics. } *)
 
-type tactic_reduction = env -> evar_map -> constr -> Constr.constr
+type tactic_reduction = env -> evar_map -> constr -> constr
 
 type change_arg = patvar_map -> constr Sigma.run
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1b5c4f660..1093b7fdc 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -79,7 +79,7 @@ let red_constant_entry n ce sigma = function
       let redfun env sigma c =
         let sigma = Sigma.Unsafe.of_evar_map sigma in
         let Sigma (c, _, _) = redfun.e_redfun env sigma c in
-        c
+        EConstr.Unsafe.to_constr c
       in
       { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
         (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
@@ -962,7 +962,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     in
       try
 	let ctx, ar = Reductionops.splay_prod_n env !evdref 2 (EConstr.of_constr relty) in
-	  match ctx, kind_of_term ar with
+	  match ctx, EConstr.kind !evdref ar with
 	  | [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null)
 	      when Reductionops.is_conv env !evdref (EConstr.of_constr t) (EConstr.of_constr u) -> t
 	  | _, _ -> error ()
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 6e63a71fd..7eb189ef5 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -87,7 +87,7 @@ let to_unsafe_judgment j = on_judgment EConstr.Unsafe.to_constr j
 
 let j_nf_betaiotaevar sigma j =
   { uj_val = Evarutil.nf_evar sigma j.uj_val;
-    uj_type = Reductionops.nf_betaiota sigma (EConstr.of_constr j.uj_type) }
+    uj_type = EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma (EConstr.of_constr j.uj_type)) }
 
 let jv_nf_betaiotaevar sigma jl =
   Array.map (j_nf_betaiotaevar sigma) jl
@@ -362,6 +362,7 @@ let explain_actual_type env sigma j t reason =
   let env = make_all_name_different env in
   let j = j_nf_betaiotaevar sigma j in
   let t = Reductionops.nf_betaiota sigma (EConstr.of_constr t) in
+  let t = EConstr.Unsafe.to_constr t in
   (** Actually print *)
   let pe = pr_ne_context_of (str "In environment") env sigma in
   let pc = pr_lconstr_env env sigma (Environ.j_val j) in
@@ -381,6 +382,7 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
   let randl = jv_nf_betaiotaevar sigma randl in
   let exptyp = Evarutil.nf_evar sigma exptyp in
   let actualtyp = Reductionops.nf_betaiota sigma (EConstr.of_constr actualtyp) in
+  let actualtyp = EConstr.Unsafe.to_constr actualtyp in
   let rator = Evarutil.j_nf_evar sigma rator in
   let rator = to_unsafe_judgment rator in
   let env = make_all_name_different env in
@@ -1115,6 +1117,7 @@ let explain_non_linear_proof c =
   spc () ++ str "because a metavariable has several occurrences."
 
 let explain_meta_in_type c =
+  let c = EConstr.Unsafe.to_constr c in
   str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++
   str " of another meta"
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index aac1d1ed4..2a0ebf402 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -264,7 +264,7 @@ let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
 let error s = pperror (str s)
 
 let reduce c =
-  Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty (EConstr.of_constr c)
+  EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty (EConstr.of_constr c))
 
 exception NoObligations of Id.t option
 
@@ -536,6 +536,8 @@ let declare_mutual_definition l =
 	let subs, typ = (subst_body true x) in
 	let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len (EConstr.of_constr subs)) in
 	let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len (EConstr.of_constr typ)) in
+	let term = EConstr.Unsafe.to_constr term in
+	let typ = EConstr.Unsafe.to_constr typ in
 	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
   in
 (*   let fixdefs = List.map reduce_fix fixdefs in *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 929505716..96221b742 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -121,6 +121,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
          | CSort (_, Misctypes.GType []) -> true | _ -> false in
        let s = interp_type_evars env evars ~impls:empty_internalization_env t in
        let sred = Reductionops.whd_all env !evars (EConstr.of_constr s) in
+       let sred = EConstr.Unsafe.to_constr sred in
 	 (match kind_of_term sred with
 	 | Sort s' -> 
 	    (if poly then
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 773766d7e..25b639fb0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1588,7 +1588,7 @@ let vernac_check_may_eval redexp glopt rc =
   match redexp with
     | None ->
         let l = Evar.Set.union (Evd.evars_of_term j.Environ.uj_val) (Evd.evars_of_term j.Environ.uj_type) in
-        let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' (EConstr.of_constr j.Environ.uj_type) } in
+        let j = { j with Environ.uj_type = EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma' (EConstr.of_constr j.Environ.uj_type)) } in
 	Feedback.msg_notice (print_judgment env sigma' j ++
                     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
                     Printer.pr_universe_ctx sigma uctx)