Evar-normalizing functions now act on EConstrs.

50 files changed, 233 insertions, 227 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 8940be09d..42620c0b5 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -99,16 +99,21 @@ let rec whd_evar sigma c =
 	if u' == u then c else mkConstructU (co, u')
     | _ -> c
 
-let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t)
-let e_nf_evar sigma t = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr t))
+(** Term exploration up to instantiation. *)
+let kind_of_term_upto sigma t =
+  Constr.kind (whd_evar sigma t)
+
+let rec nf_evar0 sigma t = Constr.map (fun t -> nf_evar0 sigma t) (whd_evar sigma t)
+let whd_evar sigma c = EConstr.of_constr (whd_evar sigma (EConstr.Unsafe.to_constr c))
+let nf_evar sigma c = EConstr.of_constr (nf_evar0 sigma (EConstr.Unsafe.to_constr c))
 
 let j_nf_evar sigma j =
-  { uj_val = e_nf_evar sigma j.uj_val;
-    uj_type = e_nf_evar sigma j.uj_type }
+  { uj_val = nf_evar sigma j.uj_val;
+    uj_type = nf_evar sigma j.uj_type }
 let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
 let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
 let tj_nf_evar sigma {utj_val=v;utj_type=t} =
-  {utj_val=e_nf_evar sigma v;utj_type=t}
+  {utj_val=nf_evar sigma v;utj_type=t}
 
 let nf_evars_universes evm =
   Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) 
@@ -125,23 +130,23 @@ let e_nf_evars_and_universes evdref =
 let nf_evar_map_universes evm =
   let evm = Evd.nf_constraints evm in
   let subst = Evd.universe_subst evm in
-    if Univ.LMap.is_empty subst then evm, nf_evar evm
+    if Univ.LMap.is_empty subst then evm, nf_evar0 evm
     else
       let f = nf_evars_universes evm in
 	Evd.raw_map (fun _ -> map_evar_info f) evm, f
 
 let nf_named_context_evar sigma ctx =
-  Context.Named.map (nf_evar sigma) ctx
+  Context.Named.map (nf_evar0 sigma) ctx
 
 let nf_rel_context_evar sigma ctx =
-  Context.Rel.map (nf_evar sigma) ctx
+  Context.Rel.map (nf_evar0 sigma) ctx
 
 let nf_env_evar sigma env =
   let nc' = nf_named_context_evar sigma (Environ.named_context env) in
   let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
     push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
 
-let nf_evar_info evc info = map_evar_info (nf_evar evc) info
+let nf_evar_info evc info = map_evar_info (nf_evar0 evc) info
 
 let nf_evar_map evm =
   Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm
@@ -527,7 +532,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
       | Evar (evk,l as ev) ->
 	  if Evd.is_defined !evdref evk then
 	    (* If evk is already defined we replace it by its definition *)
-	    let nc = whd_evar !evdref c in
+	    let nc = Evd.existential_value !evdref ev in
 	      (check_and_clear_in_constr env evdref err ids global nc)
 	  else
 	    (* We check for dependencies to elements of ids in the
@@ -582,7 +587,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
 	      let evi' = { evi with evar_extra = extra' } in
 	      evdref := Evd.add !evdref evk evi' ;
 	    (* spiwack: /hacking session *)
-              whd_evar !evdref c
+              Evd.existential_value !evdref ev
 
       | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c
 
@@ -751,10 +756,6 @@ let subterm_source evk (loc,k) =
   (loc,Evar_kinds.SubEvar evk)
 
 
-(** Term exploration up to instantiation. *)
-let kind_of_term_upto sigma t =
-  Constr.kind (whd_evar sigma t)
-
 (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
     [u] up to existential variable instantiation and equalisable
     universes. The term [t] is interpreted in [sigma1] while [u] is
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index ea9599c8b..67de18abc 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -139,8 +139,8 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
 (** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
     uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
 
-val whd_evar :  evar_map -> constr -> constr
-val nf_evar :  evar_map -> constr -> constr
+val whd_evar :  evar_map -> EConstr.constr -> EConstr.constr
+val nf_evar :  evar_map -> EConstr.constr -> EConstr.constr
 val j_nf_evar :  evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
 val jl_nf_evar :
    evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 9e5e9c7da..ab72cc405 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -24,7 +24,7 @@ type proofview = Proofview_monad.proofview
 
 (* The first items in pairs below are proofs (under construction).
    The second items in the pairs below are statements that are being proved. *)
-type entry = (Term.constr * Term.types) list
+type entry = (EConstr.constr * EConstr.types) list
 
 (** Returns a stylised view of a proofview for use by, for instance,
     ide-s. *)
@@ -37,15 +37,16 @@ let proofview p =
   p.comb , p.solution
 
 let compact el ({ solution } as pv) =
-  let nf = Evarutil.nf_evar solution in
+  let nf c = Evarutil.nf_evar solution c in
+  let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in
   let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
   let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
   let pruned_solution = Evd.drop_all_defined solution in
   let apply_subst_einfo _ ei =
     Evd.({ ei with
-       evar_concl =  nf ei.evar_concl;
-       evar_hyps = Environ.map_named_val nf ei.evar_hyps;
-       evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
+       evar_concl =  nf0 ei.evar_concl;
+       evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
+       evar_candidates = Option.map (List.map nf0) ei.evar_candidates }) in
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
   Feedback.msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
@@ -56,7 +57,7 @@ let compact el ({ solution } as pv) =
 
 type telescope =
   | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
+  | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
 
 let typeclass_resolvable = Evd.Store.field ()
 
@@ -71,11 +72,10 @@ let dependent_init =
   | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
     let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store (EConstr.of_constr typ) in
-    let econstr = EConstr.Unsafe.to_constr econstr in
+    let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in
+    let (gl, _) = EConstr.destEvar (Sigma.to_evar_map sigma) econstr in
     let sigma = Sigma.to_evar_map sigma in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
-    let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
     entry, { solution = sol; comb = gl :: comb; shelf = [] }
   in
@@ -1222,12 +1222,12 @@ module V82 = struct
    { Evd.it = comb ; sigma = solution }
 
   let top_goals initial { solution=solution; } =
-    let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in
+    let goals = CList.map (fun (t,_) -> fst (Term.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }
 
   let top_evars initial =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term c)
+      Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
     in
     CList.flatten (CList.map evars_of_initial initial)
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 2350592a2..9f10e874a 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -43,7 +43,7 @@ val compact : entry -> proofview -> entry * proofview
     empty [evar_map] (indeed a proof can be triggered by an incomplete
     pretyping), [init] takes an additional argument to represent the
     initial [evar_map]. *)
-val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
+val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofview
 
 (** A [telescope] is a list of environment and conclusion like in
     {!init}, except that each element may depend on the previous
@@ -52,7 +52,7 @@ val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview
     [evar_map] is threaded in state passing style. *)
 type telescope =
   | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
+  | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
 
 (** Like {!init}, but goals are allowed to be dependent on one
     another. Dependencies between goals is represented with the type
@@ -69,8 +69,8 @@ val finished : proofview -> bool
 (** Returns the current [evar] state. *)
 val return : proofview -> Evd.evar_map
 
-val partial_proof : entry -> proofview -> constr list
-val initial_goals : entry -> (constr * types) list
+val partial_proof : entry -> proofview -> EConstr.constr list
+val initial_goals : entry -> (EConstr.constr * EConstr.types) list
 
 
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 3f924cfa1..196962354 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -12,8 +12,8 @@
 open Pp
 open Names
 open Term
-open EConstr
 open Environ
+open EConstr
 
 (** printers *)
 val print_sort : sorts -> std_ppcmds
@@ -283,4 +283,4 @@ val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns
 
 (** {6 Functions to deal with impossible cases } *)
 val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit
-val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set
+val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index fcba01353..8fc5547ec 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -191,12 +191,11 @@ let process_goal sigma g =
   let min_env = Environ.reset_context env in
   let id = Goal.uid g in
   let ccl =
-    let norm_constr = Reductionops.nf_evar sigma (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in
-    let norm_constr = EConstr.of_constr norm_constr in
+    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
     Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
   in
   let process_hyp d (env,l) =
-    let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in
+    let d = CompactedDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_evar sigma (EConstr.of_constr c))) d in
     let d' = CompactedDecl.to_named_context d in
       (List.fold_right Environ.push_named d' env,
        (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 715929c56..c942e8e92 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -57,9 +57,6 @@ let nlocal_def (na, b, t) =
   let inj = EConstr.Unsafe.to_constr in
   NamedDecl.LocalDef (na, inj b, inj t)
 
-let nf_evar sigma c =
-  EConstr.of_constr (Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr c))
-
 (** Typeclass-based generalized rewriting. *)
 
 (** Constants used by the tactic. *)
@@ -663,7 +660,7 @@ let solve_remaining_by env sigma holes by =
         (** Evar should not be defined, but just in case *)
       | Some evi ->
         let env = Environ.reset_with_named_context evi.evar_hyps env in
-        let ty = evi.evar_concl in
+        let ty = EConstr.of_constr evi.evar_concl in
         let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in
         Evd.define evk c sigma
     in
@@ -738,7 +735,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs)
     let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
       ~fail:true env sigma in
     let evd = solve_remaining_by env sigma holes by in
-    let nf c = nf_evar evd (Reductionops.nf_meta evd c) in
+    let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in
     let c1 = nf c1 and c2 = nf c2
     and rew_car = nf car and rel = nf rel
     and prf = nf prf in
@@ -1449,7 +1446,7 @@ module Strategies =
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
-	    let c' = nf_evar sigma c in
+	    let c' = Reductionops.nf_evar sigma c in
 	      state, Success { rew_car = ty; rew_from = t; rew_to = c';
 				  rew_prf = RewCast DEFAULTcast;
 				  rew_evars = (sigma, snd evars) }
@@ -1522,7 +1519,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
     | Success res ->
       let (_, cstrs) = res.rew_evars in
       let evars' = solve_constraints env res.rew_evars in
-      let newt = nf_evar evars' res.rew_to in
+      let newt = Reductionops.nf_evar evars' res.rew_to in
       let evars = (* Keep only original evars (potentially instantiated) and goal evars,
 		     the rest has been defined and substituted already. *)
 	Evar.Set.fold 
@@ -1537,13 +1534,13 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
       let res = match res.rew_prf with
 	| RewCast c -> None
 	| RewPrf (rel, p) ->
-	  let p = nf_zeta env evars' (nf_evar evars' p) in
+	  let p = nf_zeta env evars' (Reductionops.nf_evar evars' p) in
 	  let term =
 	    match abs with
 	    | None -> p
 	    | Some (t, ty) ->
-              let t = nf_evar evars' t in
-              let ty = nf_evar evars' ty in
+              let t = Reductionops.nf_evar evars' t in
+              let ty = Reductionops.nf_evar evars' ty in
 		mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |])
 	  in
 	  let proof = match is_hyp with
@@ -2024,7 +2021,7 @@ let add_morphism_infer glob m n =
       let hook = Lemmas.mk_hook hook in
 	Flags.silently
 	  (fun () ->
-	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) instance hook;
+	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook;
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
 let add_morphism glob binders m s n =
@@ -2085,7 +2082,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env =
         ~flags:rewrite_conv_unif_flags
         env sigma ((if l2r then c1 else c2),but)
   in
-  let nf c = nf_evar sigma c in
+  let nf c = Reductionops.nf_evar sigma c in
   let c1 = if l2r then nf c' else nf c1
   and c2 = if l2r then nf c2 else nf c'
   and car = nf car and rel = nf rel in
@@ -2104,7 +2101,7 @@ let get_hyp gl (c,l) clause l2r =
   let sigma, hi = decompose_applied_relation env evars (c,l) in
   let but = match clause with
     | Some id -> Tacmach.New.pf_get_hyp_typ id gl
-    | None -> nf_evar evars (Tacmach.New.pf_concl gl)
+    | None -> Reductionops.nf_evar evars (Tacmach.New.pf_concl gl)
   in
   unification_rewrite l2r hi.c1 hi.c2 sigma hi.prf hi.car hi.rel but env
 
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 36a0336bc..62d0cc529 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -2101,7 +2101,6 @@ let interp_redexp env sigma r =
 
 let _ =
   let eval ty env sigma lfun arg =
-    let ty = EConstr.Unsafe.to_constr ty in
     let ist = { lfun = lfun; extra = TacStore.empty; } in
     if Genarg.has_type arg (glbwit wit_tactic) then
       let tac = Genarg.out_gen (glbwit wit_tactic) arg in
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 6a0ec3968..da971fffb 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1506,6 +1506,7 @@ let rec postprocess pts instr =
     | Pend (B_elim ET_Induction) ->
   	begin
 	  let pfterm = List.hd (Proof.partial_proof pts) in
+	  let pfterm = EConstr.Unsafe.to_constr pfterm in
 	  let { it = gls ; sigma = sigma } = Proof.V82.subgoals pts in
 	  let env =  try
 		       Goal.V82.env sigma (List.hd gls)
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index f23f4ce7d..12d7f0660 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -28,16 +28,17 @@ let start_deriving f suchthat lemma =
   (* spiwack: I don't know what the rigidity flag does, picked the one
      that looked the most general. *)
   let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in
-  let f_type_type = Term.mkSort f_type_sort in
+  let f_type_type = EConstr.mkSort f_type_sort in
   (** create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *)
   let goals =
     let open Proofview in
         TCons ( env , sigma , f_type_type , (fun sigma f_type ->
         TCons ( env , sigma , f_type , (fun sigma ef ->
+        let f_type = EConstr.Unsafe.to_constr f_type in
+        let ef = EConstr.Unsafe.to_constr ef in
         let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
         let evdref = ref sigma in
         let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
-        let suchthat = EConstr.Unsafe.to_constr suchthat in
         TCons ( env' , !evdref , suchthat , (fun sigma _ ->
         TNil sigma))))))
     in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f4fa61a22..91b17b9a4 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1007,7 +1007,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
     (mk_equation_id f_id)
     (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem))
     evd
-  (EConstr.Unsafe.to_constr lemma_type)
+  lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
   Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index ba01b3b04..d0d44b34b 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -294,7 +294,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
       new_princ_name
       (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem))
       !evd
-      new_principle_type
+      (EConstr.of_constr new_principle_type)
       hook
   ;
     (*       let _tim1 = System.get_time ()  in *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 5cbec7743..dcec2cb74 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -846,7 +846,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	   lem_id
 	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem)))
            !evd
-	   (EConstr.Unsafe.to_constr typ)
+	   typ
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
@@ -908,7 +908,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
-	 (EConstr.Unsafe.to_constr (fst lemmas_types_infos.(i)))
+	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index adbdb1eb7..56c6ab054 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1374,7 +1374,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
   Lemmas.start_proof
     na
     (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
-    sigma (EConstr.Unsafe.to_constr gls_type)
+    sigma gls_type
     (Lemmas.mk_hook hook);
   if Indfun_common.is_strict_tcc  ()
   then
@@ -1421,7 +1421,7 @@ let com_terminate
     let (evmap, env) = Lemmas.get_current_context() in
     Lemmas.start_proof thm_name
       (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
-      ctx (compute_terminate_type nb_args fonctional_ref) hook;
+      ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook;
 
     ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
     ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
@@ -1476,7 +1476,7 @@ let (com_eqn : int -> Id.t ->
     (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
        ~sign:(Environ.named_context_val env)
        evmap
-       equation_lemma_type
+       (EConstr.of_constr equation_lemma_type)
        (Lemmas.mk_hook (fun _ _ -> ()));
      ignore (by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index eb5f401e3..bf3e2ac1c 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -178,6 +178,9 @@ let mk_lterm = mk_term ' '
 
 let pf_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl)  sigma, ty
 
+let nf_evar sigma c =
+  EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c))
+
 (* }}} *)
 
 (** Profiling {{{ *************************************************************)
@@ -780,13 +783,13 @@ let on_instance, instances =
 let rec uniquize = function
   | [] -> []
   | (sigma,_,{ up_f = f; up_a = a; up_t = t } as x) :: xs ->
-    let t = Reductionops.nf_evar sigma t in
-    let f = Reductionops.nf_evar sigma f in
-    let a = Array.map (Reductionops.nf_evar sigma) a in
+    let t = nf_evar sigma t in
+    let f = nf_evar sigma f in
+    let a = Array.map (nf_evar sigma) a in
     let neq (sigma1,_,{ up_f = f1; up_a = a1; up_t = t1 }) =
-      let t1 = Reductionops.nf_evar sigma1 t1 in
-      let f1 = Reductionops.nf_evar sigma1 f1 in
-      let a1 = Array.map (Reductionops.nf_evar sigma1) a1 in
+      let t1 = nf_evar sigma1 t1 in
+      let f1 = nf_evar sigma1 f1 in
+      let a1 = Array.map (nf_evar sigma1) a1 in
       not (Term.eq_constr t t1 &&
            Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in
     x :: uniquize (List.filter neq xs) in
@@ -1138,7 +1141,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
           if k = h_k || List.mem k acc || Evd.mem sigma0 k then acc else
           (update k; k::acc)
       | _ -> fold_constr aux acc t in 
-      aux [] (Evarutil.nf_evar sigma rp) in
+      aux [] (nf_evar sigma rp) in
     let sigma = 
       List.fold_left (fun sigma e ->
         if Evd.is_defined sigma e then sigma else (* clear may be recursive *)
@@ -1195,7 +1198,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
     let sigma, rp = interp_term ist gl rp in
     let _, h, _, rp = destLetIn rp in
     let sigma = cleanup_XinE h x rp sigma in
-    let rp = subst1 h (Evarutil.nf_evar sigma rp) in
+    let rp = subst1 h (nf_evar sigma rp) in
     sigma, mk h rp
   | E_In_X_In_T(e, x, rp) | E_As_X_In_T (e, x, rp) ->
     let mk e x p =
@@ -1204,7 +1207,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
     let sigma, rp = interp_term ist gl rp in
     let _, h, _, rp = destLetIn rp in
     let sigma = cleanup_XinE h x rp sigma in
-    let rp = subst1 h (Evarutil.nf_evar sigma rp) in
+    let rp = subst1 h (nf_evar sigma rp) in
     let sigma, e = interp_term ist (re_sig (sig_it gl) sigma) e in
     sigma, mk e h rp
 ;;
@@ -1220,7 +1223,7 @@ let noindex = Some(false,[])
 
 (* calls do_subst on every sub-term identified by (pattern,occ) *)
 let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
-  let fs sigma x = Reductionops.nf_evar sigma x in
+  let fs sigma x = nf_evar sigma x in
   let pop_evar sigma e p =
     let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in
     let e_body = match e_body with Evar_defined c -> c
@@ -1307,7 +1310,7 @@ let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) =
   let sigma =
     if not resolve_typeclasses then sigma
     else Typeclasses.resolve_typeclasses ~fail:false env sigma in
-  Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma
+  nf_evar sigma e, Evd.evar_universe_context sigma
 
 let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h =
   let do_make_rel, occ =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index eea94f021..0e4c6619b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -362,7 +362,7 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
   let j = typing_fun tycon env evdref tomatch in
   let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in
   evdref := evd;
-  let typ = EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr j.uj_type)) in
+  let typ = nf_evar !evdref j.uj_type in
   let t =
     try try_find_ind env !evdref typ realnames
     with Not_found ->
@@ -1145,7 +1145,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
   let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with
   | [], _ -> brs,tomatch,pred,[]
   | n::deps, Abstract (i,d) :: tomatch ->
-      let d = map_constr (nf_evar evd) d in
+      let d = map_constr (fun c -> EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c))) d in
       let is_d = match d with LocalAssum _ -> false | LocalDef _ -> true in
       if is_d || List.exists (fun c -> dependent_decl evd (lift k c) d) tocheck
                  && Array.exists (is_dependent_branch evd k) brs then
@@ -2008,9 +2008,9 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
       let envar = List.fold_right push_rel_context arsign env in
       let sigma, newt = new_sort_variable univ_flexible_alg sigma in
       let evdref = ref sigma in
-      let predcclj = typing_fun (mk_tycon (EConstr.mkSort newt)) envar evdref rtntyp in
+      let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
       let sigma = !evdref in
-      let predccl = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr predcclj.uj_val)) in
+      let predccl = nf_evar sigma predcclj.uj_val in
       [sigma, predccl]
   in
   List.map
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ead44cee2..91f53a886 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -417,7 +417,6 @@ let inh_tosort_force loc env evd j =
   try
     let t,p = lookup_path_to_sort_from env evd j.uj_type in
     let evd,j1 = apply_coercion env evd p j t in
-    let whd_evar evd c = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr c)) in
     let j2 = on_judgment_type (whd_evar evd) j1 in
       (evd,type_judgment env evd j2)
   with Not_found | NoCoercion ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 87267d538..3ae2e35e6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -526,7 +526,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  | None, Success i' ->
             (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *)
             (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *)
-	    let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev1))) in
+	    let ev1' = whd_evar i' (mkEvar ev1) in
 	      if isEvar i' ev1' then
 		solve_simple_eqn (evar_conv_x ts) env i'
 		  (position_problem true pbty,destEvar i' ev1', term2)
@@ -536,7 +536,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  | Some (r,[]), Success i' ->
             (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
             (* we now unify r[?ev1] and ?ev2 *)
-	    let ev2' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev2))) in
+	    let ev2' = whd_evar i' (mkEvar ev2) in
 	      if isEvar i' ev2' then
 		solve_simple_eqn (evar_conv_x ts) env i'
 		  (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r))
@@ -547,7 +547,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             (* Symmetrically *)
             (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
             (* we now unify ?ev1 and r[?ev2] *)
-	    let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (mkEvar ev1))) in
+	    let ev1' = whd_evar i' (mkEvar ev1) in
 	      if isEvar i' ev1' then
 		solve_simple_eqn (evar_conv_x ts) env i'
 	          (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r))
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 875e4a118..5831d3191 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -33,8 +33,9 @@ let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal t
   (Sigma.to_evar_map evd, evk)
 
 let env_nf_evar sigma env =
+  let nf_evar c = EConstr.Unsafe.to_constr (nf_evar sigma (EConstr.of_constr c)) in
   process_rel_context
-    (fun d e -> push_rel (RelDecl.map_constr (nf_evar sigma) d) e) env
+    (fun d e -> push_rel (RelDecl.map_constr nf_evar d) e) env
 
 let env_nf_betaiotaevar sigma env =
   process_rel_context
@@ -144,7 +145,7 @@ let define_pure_evar_as_lambda env evd evk =
   | _ -> error_not_product env evd typ in
   let avoid = ids_of_named_context (evar_context evi) in
   let id =
-    next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd (EConstr.Unsafe.to_constr dom)) in
+    next_name_away_with_default_using_types "x" na avoid (EConstr.Unsafe.to_constr (Reductionops.whd_evar evd dom)) in
   let newenv = push_named (nlocal_assum (id, dom)) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = evar_source evk evd1 in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index de2e46a78..3235c2505 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -601,13 +601,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
   let evd = Sigma.Unsafe.of_evar_map evd in
   let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
   let evd = Sigma.to_evar_map evd in
-  let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in
+  let t_in_env = whd_evar evd t_in_env in
   let (evk, _) = destEvar evd evar_in_env in
   let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
   let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
   let evar_in_sign = mkEvar (evk, inst_in_sign) in
-  (evd,EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign)))
+  (evd,whd_evar evd evar_in_sign)
 
 (* We have x1..xq |- ?e1 : τ and had to solve something like
  * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 673554005..24f6d1689 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -10,50 +10,51 @@ open Util
 open Names
 open Term
 open Environ
+open EConstr
 open Type_errors
 
 type unification_error =
-  | OccurCheck of existential_key * EConstr.constr
-  | NotClean of EConstr.existential * env * EConstr.constr (* Constr is a variable not in scope *)
+  | OccurCheck of existential_key * constr
+  | NotClean of existential * env * constr (* Constr is a variable not in scope *)
   | NotSameArgSize
   | NotSameHead
   | NoCanonicalStructure
-  | ConversionFailed of env * EConstr.constr * EConstr.constr (* Non convertible closed terms *)
+  | ConversionFailed of env * constr * constr (* Non convertible closed terms *)
   | MetaOccurInBody of existential_key
-  | InstanceNotSameType of existential_key * env * EConstr.types * EConstr.types
+  | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
   | CannotSolveConstraint of Evd.evar_constraint * unification_error
   | ProblemBeyondCapabilities
 
 type position = (Id.t * Locus.hyp_location_flag) option
 
-type position_reporting = (position * int) * EConstr.t
+type position_reporting = (position * int) * constr
 
-type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option
+type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option
 
-type type_error = (EConstr.constr, EConstr.types) ptype_error
+type type_error = (constr, types) ptype_error
 
 type pretype_error =
   (* Old Case *)
-  | CantFindCaseType of EConstr.constr
+  | CantFindCaseType of constr
   (* Type inference unification *)
-  | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
+  | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
   (* Tactic unification *)
-  | UnifOccurCheck of existential_key * EConstr.constr
+  | UnifOccurCheck of existential_key * constr
   | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
-  | CannotUnify of EConstr.constr * EConstr.constr * unification_error option
-  | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr
+  | CannotUnify of constr * constr * unification_error option
+  | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
-  | NoOccurrenceFound of EConstr.constr * Id.t option
-  | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (env * type_error) option
-  | WrongAbstractionType of Name.t * EConstr.constr * EConstr.types * EConstr.types
+  | NoOccurrenceFound of constr * Id.t option
+  | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+  | WrongAbstractionType of Name.t * constr * types * types
   | AbstractionOverMeta of Name.t * Name.t
-  | NonLinearUnification of Name.t * EConstr.constr
+  | NonLinearUnification of Name.t * constr
   (* Pretyping *)
   | VarNotFound of Id.t
-  | UnexpectedType of EConstr.constr * EConstr.constr
-  | NotProduct of EConstr.constr
+  | UnexpectedType of constr * constr
+  | NotProduct of constr
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
   | UnsatisfiableConstraints of
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 7cef14339..c303d5d94 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -45,8 +45,8 @@ type pretype_error =
   | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
   | CannotUnify of constr * constr * unification_error option
   | CannotUnifyLocal of constr * constr * constr
-  | CannotUnifyBindingType of Constr.constr * Constr.constr
-  | CannotGeneralize of Constr.constr
+  | CannotUnifyBindingType of constr * constr
+  | CannotGeneralize of constr
   | NoOccurrenceFound of constr * Id.t option
   | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
   | WrongAbstractionType of Name.t * constr * types * types
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6b6800ac6..4660978df 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -143,9 +143,6 @@ let nf_fix sigma (nas, cs, ts) =
   let inj c = EConstr.to_constr sigma c in
   (nas, Array.map inj cs, Array.map inj ts)
 
-let nf_evar sigma c =
-  EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr c))
-
 let search_guard loc env possible_indexes fixdefs =
   (* Standard situation with only one possibility for each fix. *)
   (* We treat it separately in order to get proper error msg. *)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 8aaeeb2c2..dcc11cfcf 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -156,11 +156,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 -> Constr.constr
+val nf_evar : evar_map -> constr -> constr
 
 (** Lazy strategy, weak head reduction *)
 
-val whd_evar :  evar_map -> Constr.constr -> Constr.constr
+val whd_evar :  evar_map -> constr -> constr
 val whd_nored : local_reduction_function
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 7baff421f..e6f1e46b6 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -252,7 +252,7 @@ let judge_of_letin env name defj typj j =
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env evdref cstr =
-  let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
+  let cstr = whd_evar !evdref cstr in
   match EConstr.kind !evdref cstr with
     | Meta n ->
         { uj_val = cstr; uj_type = meta_type !evdref n }
@@ -411,6 +411,6 @@ let e_solve_evars env evdref c =
   let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
-  EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr c))
+  nf_evar !evdref c
 
 let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 20f27a15a..1dc3ccdc0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -137,7 +137,7 @@ let abstract_list_all_with_dependencies env evd typ c l =
     Evarconv.second_order_matching empty_transparent_state
       env evd ev' argoccs c in
   if b then
-    let p = nf_evar evd (EConstr.Unsafe.to_constr ev) in
+    let p = nf_evar evd ev in
       evd, p
   else error_cannot_find_well_typed_abstraction env evd 
     c l None
@@ -1240,7 +1240,7 @@ let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
   let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in
   let evd' = Evarconv.consider_remaining_unif_problems env evd' in
-  let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
+  let evd' = Evd.map_metas_fvalue (fun c -> EConstr.Unsafe.to_constr (nf_evar evd' (EConstr.of_constr c))) evd' in
     (evd',j'.uj_val)
 
 let w_coerce_to_type env evd c cty mvty =
@@ -1397,7 +1397,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
     let evd''' = w_merge_rec evd'' mc ec [] in
     if evd' == evd'''
     then Evd.define sp (EConstr.Unsafe.to_constr c) evd'''
-    else Evd.define sp (Evarutil.nf_evar evd''' (EConstr.Unsafe.to_constr c)) evd''' in
+    else Evd.define sp (EConstr.Unsafe.to_constr (Evarutil.nf_evar evd''' c)) evd''' in
 
   let check_types evd = 
     let metas = Evd.meta_list evd in
@@ -1513,8 +1513,7 @@ let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sig
   let current_sigma = Sigma.to_evar_map current_sigma in
   let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
   let sigma, subst = nf_univ_variables sigma in
-  let c = EConstr.Unsafe.to_constr c in
-  Sigma.Unsafe.of_pair (EConstr.of_constr (CVars.subst_univs_constr subst (nf_evar sigma c)), sigma)
+  Sigma.Unsafe.of_pair (EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))), sigma)
 
 let default_matching_core_flags sigma =
   let ts = Names.full_transparent_state in {
@@ -1602,7 +1601,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 (EConstr.Unsafe.to_constr (local_strong whd_meta sigma c))), l) in
+     let c = applist (nf_evar sigma (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))))
 
@@ -1926,7 +1925,6 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
 let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
   let typp = Typing.meta_type evd p in
   let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in
-  let pred = EConstr.of_constr pred in
   w_merge env false flags.merge_unify_flags
     (evd,[p,pred,(Conv,TypeProcessed)],[])
 
diff --git a/printing/printer.ml b/printing/printer.ml
index ba4b68296..63aeec82c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -506,8 +506,8 @@ let print_evar_constraints gl sigma =
        end
   in
   let pr_evconstr (pbty,env,t1,t2) =
-    let t1 = Evarutil.nf_evar sigma t1
-    and t2 = Evarutil.nf_evar sigma t2 in
+    let t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1)
+    and t2 = Evarutil.nf_evar sigma (EConstr.of_constr t2) in
     let env =
       (** We currently allow evar instances to refer to anonymous de Bruijn
           indices, so we protect the error printing code in this case by giving
@@ -517,11 +517,11 @@ let print_evar_constraints gl sigma =
           naming/renaming *)
       Namegen.make_all_name_different env in
     str" " ++
-      hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++
+      hov 2 (pr_env env ++ pr_leconstr_env env sigma t1 ++ spc () ++
              str (match pbty with
                   | Reduction.CONV -> "=="
                   | Reduction.CUMUL -> "<=") ++
-             spc () ++ pr_lconstr_env env sigma t2)
+             spc () ++ pr_leconstr_env env sigma t2)
   in
   let pr_candidate ev evi (candidates,acc) =
     if Option.has_some evi.evar_candidates then
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index af910810b..142fd9a89 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -199,6 +199,7 @@ let refine_by_tactic env sigma ty tac =
   | _ -> assert false
   in
   let ans = Reductionops.nf_evar sigma ans in
+  let ans = EConstr.Unsafe.to_constr ans in
   (** [neff] contains the freshly generated side-effects *)
   let neff = Evd.eval_side_effects sigma in
   (** Reset the old side-effects *)
@@ -232,7 +233,8 @@ let solve_by_implicit_tactic env sigma evk =
       let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
       (try
         let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
-        if Evarutil.has_undefined_evars sigma (EConstr.of_constr c) then raise Exit;
+        let c = EConstr.of_constr c in
+        if Evarutil.has_undefined_evars sigma c then raise Exit;
         let (ans, _, ctx) =
 	  build_by_tactic env (Evd.evar_universe_context sigma) c tac in
         let sigma = Evd.set_universe_context sigma ctx in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 807a554df..516125ea1 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -60,7 +60,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards
 type universe_binders = Id.t Loc.located list
 
 val start_proof :
-  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
+  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -106,7 +106,7 @@ val get_current_context : unit -> Evd.evar_map * env
 (** [current_proof_statement] *)
 
 val current_proof_statement :
-  unit -> Id.t * goal_kind * types
+  unit -> Id.t * goal_kind * EConstr.types
 
 (** {6 ... } *)
 (** [get_current_proof_name ()] return the name of the current focused
@@ -166,15 +166,15 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 
 val build_constant_by_tactic :
   Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
-  types -> unit Proofview.tactic -> 
+  EConstr.types -> unit Proofview.tactic -> 
   Safe_typing.private_constants Entries.definition_entry * bool *
     Evd.evar_universe_context
 
 val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
-  types -> unit Proofview.tactic -> 
+  EConstr.types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
-val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic ->
+val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic ->
   constr * Evd.evar_map
 (** A variant of the above function that handles open terms as well.
     Caveat: all effects are purged in the returned term at the end, but other
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 5053fc7fb..8dcc5b76e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -66,9 +66,9 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
 
 (*** General proof functions ***)
 
-val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
+val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
 val dependent_start : Proofview.telescope -> proof
-val initial_goals : proof -> (Term.constr * Term.types) list
+val initial_goals : proof -> (EConstr.constr * EConstr.types) list
 val initial_euctx : proof -> Evd.evar_universe_context
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
@@ -79,7 +79,7 @@ val is_done : proof -> bool
 val is_complete : proof -> bool
 
 (* Returns the list of partial proofs to initial goals. *)
-val partial_proof : proof -> Term.constr list
+val partial_proof : proof -> EConstr.constr list
 
 val compact : proof -> proof
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2956d623f..eb1bea897 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -375,6 +375,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   in
   let entries =
     Future.map2 (fun p (_, t) ->
+      let t = EConstr.Unsafe.to_constr t in
       let univstyp, body = make_body t p in
       let univs, typ = Future.force univstyp in
 	{ Entries.
@@ -406,7 +407,7 @@ let return_proof ?(allow_partial=false) () =
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
-  let proofs = List.map (fun c -> c, eff) proofs in
+  let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
     proofs, Evd.evar_universe_context evd
  end else
   let initial_goals = Proof.initial_goals proof in
@@ -430,7 +431,7 @@ let return_proof ?(allow_partial=false) () =
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
   let proofs = 
-    List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in
+    List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 97a21cf22..3b2cc6b23 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -86,7 +86,7 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
     end of the proof to close the proof. *)
 val start_proof :
   Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
-  Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
+  Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
@@ -201,7 +201,7 @@ end
 val get_default_goal_selector : unit -> Vernacexpr.goal_selector
 
 module V82 : sig
-  val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list *
+  val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
   Decl_kinds.goal_kind)
 end
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 2fab026ea..3ed262d6e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -223,7 +223,7 @@ module New = struct
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = project gl in
-    EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr concl))
+    nf_evar sigma concl
 
   let pf_whd_all gl t = pf_apply whd_all gl t
 
@@ -241,6 +241,6 @@ module New = struct
   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 = EConstr.of_constr (nf_evar (project gl) (EConstr.Unsafe.to_constr t))
+  let pf_nf_evar gl t = nf_evar (project gl) t
 
 end
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index e3f1c1ac2..77fb960e1 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+      start_proof_univs id ?pl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
 let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
@@ -461,13 +461,12 @@ let start_proof_com ?inference_hook kind thms hook =
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
-    let t' = EConstr.Unsafe.to_constr t' in
     let flags = all_and_fail_flags in
     let flags = { flags with use_hook = inference_hook } in
     evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
     let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
-      (nf_evar !evdref (Term.it_mkProd_or_LetIn t' ctx),
+      (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)),
        (ids, imps @ lift_implicits (List.length ids) imps'),
        guard)))
     thms in
@@ -519,6 +518,7 @@ let save_proof ?proof = function
         | None ->
             let pftree = Pfedit.get_pftreestate () in
             let id, k, typ = Pfedit.current_proof_statement () in
+            let typ = EConstr.Unsafe.to_constr typ in
             let universes = Proof.initial_euctx pftree in
             (* This will warn if the proof is complete *)
             let pproofs, _univs =
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 39c089be9..681413a29 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -19,17 +19,17 @@ val call_hook :
   Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
 
 (** A hook start_proof calls on the type of the definition being started *)
-val set_start_hook : (types -> unit) -> unit
+val set_start_hook : (EConstr.types -> unit) -> unit
 
 val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
   ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val -> types ->
+  ?sign:Environ.named_context_val -> EConstr.types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
 val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
   ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val -> types ->
+  ?sign:Environ.named_context_val -> EConstr.types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
   (Evd.evar_universe_context option -> unit declaration_hook) -> unit
 
diff --git a/stm/stm.ml b/stm/stm.ml
index d60412c0c..47e806929 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1719,8 +1719,10 @@ end = struct (* {{{ *)
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> RespNoProgress
         | Evd.Evar_defined t ->
+            let t = EConstr.of_constr t in
             let t = Evarutil.nf_evar sigma t in
-            if Evarutil.is_ground_term sigma (EConstr.of_constr t) then
+            if Evarutil.is_ground_term sigma t then
+              let t = EConstr.Unsafe.to_constr t in
               RespBuiltSubProof (t, Evd.evar_universe_context sigma)
             else CErrors.user_err ~hdr:"STM" (str"The solution is not ground")
        end) ()
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b548f8b92..17a488ddb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -321,7 +321,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
       ( Proofview.Goal.enter { enter = begin fun gl ->
           let sigma = Tacmach.New.project gl in
           let env = Proofview.Goal.env gl in
-          let nf c = Evarutil.nf_evar sigma c in
+          let nf c = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)) in
           let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
           let hyp = Context.Named.Declaration.map_constr nf decl in
 	  let hintl = make_resolve_hyp env sigma hyp
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index fa2c21ac3..a4b6cb53b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -521,8 +521,7 @@ let evars_to_goals p evm =
 (** Making local hints  *)
 let make_resolve_hyp env sigma st flags only_classes pri decl =
   let id = NamedDecl.get_id decl in
-  let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in
-  let cty = EConstr.of_constr cty in
+  let cty = Evarutil.nf_evar sigma (EConstr.of_constr (NamedDecl.get_type decl)) in
   let rec iscl env ty =
     let ctx, ar = decompose_prod_assum sigma ty in
       match EConstr.kind sigma (fst (decompose_app sigma ar)) with
@@ -1476,8 +1475,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
   in
   let evd = sig_sig gls' in
   let t' = mkEvar (ev, Array.of_list subst) in
-  let term = Evarutil.nf_evar evd (EConstr.Unsafe.to_constr t') in
-  let term = EConstr.of_constr term in
+  let term = Evarutil.nf_evar evd t' in
     evd, term
 
 let _ =
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index a3a448aad..7173fb4fd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -66,8 +66,7 @@ let contradiction_context =
       | [] ->  Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
       | d :: rest ->
           let id = NamedDecl.get_id d in
-          let typ = nf_evar sigma (NamedDecl.get_type d) in
-          let typ = EConstr.of_constr typ in
+          let typ = nf_evar sigma (EConstr.of_constr (NamedDecl.get_type d)) in
 	  let typ = whd_all env sigma typ in
 	  if is_empty_type sigma typ then
 	    simplest_elim (mkVar id)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 01f21910c..7453fff5c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -289,8 +289,7 @@ module SearchProblem = struct
       in
       let rec_tacs =
 	let l =
-          let concl = Reductionops.nf_evar (project g) (EConstr.Unsafe.to_constr (pf_concl g)) in
-          let concl = EConstr.of_constr concl in
+          let concl = Reductionops.nf_evar (project g) (pf_concl g) in
 	  filter_tactics s.tacres
                          (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
 	in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c80cf4416..072da995d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1212,7 +1212,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	    error "Cannot solve a unification problem."
   in
   let scf = sigrec_clausal_form siglen ty in
-    !evdref, EConstr.of_constr (Evarutil.nf_evar !evdref (EConstr.Unsafe.to_constr scf))
+    !evdref, Evarutil.nf_evar !evdref scf
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 851e9f01f..ef97b0b33 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1200,7 +1200,8 @@ let prepare_hint check (poly,local) env init (sigma,c) =
      It is actually a bit stupid to generalize over evars since the first
      thing make_resolves will do is to re-instantiate the products *)
   let sigma, subst = Evd.nf_univ_variables sigma in
-  let c = Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr c) in
+  let c = Evarutil.nf_evar sigma c in
+  let c = EConstr.Unsafe.to_constr c in
   let c = CVars.subst_univs_constr subst c in
   let c = EConstr.of_constr c in
   let c = drop_extra_implicit_args sigma c in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 3199623e7..a05b4fbf3 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -208,14 +208,12 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     user_err ~hdr:"lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
-  let invGoal = EConstr.Unsafe.to_constr invGoal in
   let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
   let pf =
     fst (Proof.run_tactic env (
       tclTHEN intro (onLastHypId inv_op)) pf)
   in
   let pfterm = List.hd (Proof.partial_proof pf) in
-  let pfterm = EConstr.of_constr pfterm in
   let global_named_context = Global.named_context_val () in
   let ownSign = ref begin
     fold_named_context
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 10582288c..0ecccd5c0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2945,7 +2945,6 @@ let quantify lconstr =
 (* Modifying/Adding an hypothesis  *)
 
 let specialize (c,lbind) ipat =
-  let nf_evar sigma c = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr c)) in
   Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
@@ -3825,7 +3824,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 ty' = EConstr.of_constr (Evarutil.nf_evar !evars (EConstr.Unsafe.to_constr ty')) in
+  let ty' = Evarutil.nf_evar !evars ty' in
     if worked then
       tclTHENFIRST (Tacmach.internal_cut true id ty')
 	(Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl
@@ -4951,6 +4950,7 @@ let abstract_subproof id gk tac =
     let ctx = Evd.universe_context_set evd in
       evd, ctx, nf concl
   in
+  let concl = EConstr.of_constr concl in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
   let ectx = Evd.evar_universe_context evd in
   let (const, safe, ectx) =
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 5e686c41e..14071d869 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -658,6 +658,7 @@ let make_bl_scheme mode mind =
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
   let ctx = Evd.make_evar_universe_context (Global.env ()) None in
   let side_eff = side_effect_of_mode mode in
+  let bl_goal = EConstr.of_constr bl_goal in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal
     (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
   in
@@ -783,6 +784,7 @@ let make_lb_scheme mode mind =
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
   let ctx = Evd.make_evar_universe_context (Global.env ()) None in
   let side_eff = side_effect_of_mode mode in
+  let lb_goal = EConstr.of_constr lb_goal in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal
     (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
@@ -956,7 +958,7 @@ let make_eq_decidability mode mind =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx
-    (compute_dec_goal (ind,u) lnamesparrec nparrec)
+    (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
     (compute_dec_tact ind lnamesparrec nparrec)
   in
   ([|ans|], ctx), Safe_typing.empty_private_constants
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 5087aa0c8..7a5d0ed81 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -181,7 +181,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
   let env' = push_rel_context ctx env in
   evars := Evarutil.nf_evar_map !evars;
   evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars;
-  let subst = List.map (Evarutil.nf_evar !evars) subst in
+  let subst = List.map (fun c -> EConstr.Unsafe.to_constr (Evarutil.nf_evar !evars (EConstr.of_constr c))) subst in
     if abstract then
       begin
 	let subst = List.fold_left2
@@ -327,7 +327,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
                      the refinement manually.*)
 		let gls = List.rev (Evd.future_goals evm) in
                 let evm = Evd.reset_future_goals evm in
-                Lemmas.start_proof id kind evm termtype
+                Lemmas.start_proof id kind evm (EConstr.of_constr termtype)
 		(Lemmas.mk_hook
                   (fun _ -> instance_hook k pri global imps ?hook));
                  (* spiwack: I don't know what to do with the status here. *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7e3828131..44fc4eb1a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -306,7 +306,8 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
     (env,empty_internalization_env) l
   in
   let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in
-  let l = List.map (on_pi2 (nf_evar evd)) l in
+  let nf_evar c = EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c)) in
+  let l = List.map (on_pi2 nf_evar) l in
   snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) ->
     let t = replace_vars subst t in
     let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in
@@ -465,7 +466,7 @@ let sign_level env evd sign =
       | LocalDef _ -> lev, push_rel d env
       | LocalAssum _ ->
 	let s = destSort (Reduction.whd_all env 
-			    (nf_evar evd (EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))))
+			    (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))))
 	in
 	let u = univ_of_sort s in
 	  (Univ.sup u lev, push_rel d env))
@@ -905,8 +906,9 @@ let fix_sub_ref = make_ref fixsub_module "Fix_sub"
 let measure_on_R_ref = make_ref fixsub_module "MR"
 let well_founded = init_constant ["Init"; "Wf"] "well_founded"
 let mkSubset name typ prop =
-  mkApp (Universes.constr_of_global (delayed_force build_sigma).typ,
-	 [| typ; mkLambda (name, typ, prop) |])
+  let open EConstr in
+  EConstr.Unsafe.to_constr (mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).typ),
+	 [| typ; mkLambda (name, typ, prop) |]))
 let sigT = Lazy.from_fun build_sigma_type
 
 let make_qref s = Qualid (Loc.ghost, qualid_of_string s)
@@ -943,9 +945,11 @@ let rec telescope = function
       ty, (LocalDef (n, b, t) :: subst), lift 1 term
 
 let nf_evar_context sigma ctx =
-  List.map (map_constr (Evarutil.nf_evar sigma)) ctx
+  List.map (map_constr (fun c -> EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)))) ctx
 
 let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
+  let open EConstr in
+  let open Vars in
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
   let ctx = Evd.make_evar_universe_context env pl in
@@ -954,11 +958,12 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
   let top_arity = interp_type_evars top_env evdref arityc in
-  let top_arity = EConstr.Unsafe.to_constr top_arity in
-  let full_arity = Term.it_mkProd_or_LetIn top_arity binders_rel in
+  let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
   let argtyp, letbinders, make = telescope binders_rel in
+  let make = EConstr.of_constr make in
   let argname = Id.of_string "recarg" in
   let arg = LocalAssum (Name argname, argtyp) in
+  let argtyp = EConstr.of_constr argtyp in
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
   let rel, _ = interp_constr_evars_impls env evdref r in
@@ -977,22 +982,21 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
 	  | _, _ -> error ()
       with e when CErrors.noncritical e -> error ()
   in
-  let rel = EConstr.Unsafe.to_constr rel in
   let measure = interp_casted_constr_evars binders_env evdref measure relargty in
-  let measure = EConstr.Unsafe.to_constr measure in
   let wf_rel, wf_rel_fun, measure_fn =
     let measure_body, measure =
       it_mkLambda_or_LetIn measure letbinders,
       it_mkLambda_or_LetIn measure binders
     in
-    let comb = Universes.constr_of_global (delayed_force measure_on_R_ref) in
+    let comb = EConstr.of_constr (Universes.constr_of_global (delayed_force measure_on_R_ref)) in
+    let relargty = EConstr.of_constr relargty in
     let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
     let wf_rel_fun x y =
       mkApp (rel, [| subst1 x measure_body;
  		     subst1 y measure_body |])
     in wf_rel, wf_rel_fun, measure
   in
-  let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
+  let wf_proof = mkApp (EConstr.of_constr (delayed_force well_founded), [| argtyp ; wf_rel |]) in
   let argid' = Id.of_string (Id.to_string argname ^ "'") in
   let wfarg len = LocalAssum (Name argid',
                               mkSubset (Name argid') argtyp
@@ -1000,7 +1004,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   in
   let intern_bl = wfarg 1 :: [arg] in
   let _intern_env = push_rel_context intern_bl env in
-  let proj = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1 in
+  let proj = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.proj1) in
   let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
   let projection = (* in wfarg :: arg :: before *)
     mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -1009,17 +1013,21 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let intern_arity = substl [projection] top_arity_let in
   (* substitute the projection of wfarg for something,
      now intern_arity is in wfarg :: arg *)
-  let intern_fun_arity_prod = Term.it_mkProd_or_LetIn intern_arity [wfarg 1] in
+  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
+  let intern_fun_arity_prod = EConstr.Unsafe.to_constr intern_fun_arity_prod in
   let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
   let curry_fun =
     let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
-    let intro = (*FIXME*)Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro in
+    let intro = (*FIXME*)EConstr.of_constr (Universes.constr_of_global (delayed_force build_sigma).Coqlib.intro) in
     let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
     let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
     let rcurry = mkApp (rel, [| measure; lift len measure |]) in
+    let rcurry = EConstr.Unsafe.to_constr rcurry in
     let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in
     let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
-    let ty = Term.it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
+    let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
+    let body = EConstr.Unsafe.to_constr body in
+    let ty = EConstr.Unsafe.to_constr ty in
       LocalDef (Name recname, body, ty)
   in
   let fun_bl = intern_fun_binder :: [arg] in
@@ -1028,26 +1036,24 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in
     let (r, l, impls, scopes) =
       Constrintern.compute_internalization_data env
-	Constrintern.Recursive full_arity impls 
+	Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls 
     in
     let newimpls = Id.Map.singleton recname
       (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
        scopes @ [None]) in
       interp_casted_constr_evars (push_rel_context ctx env) evdref
-        ~impls:newimpls body (lift 1 top_arity)
+        ~impls:newimpls body (EConstr.Unsafe.to_constr (lift 1 top_arity))
   in
-  let intern_body = EConstr.Unsafe.to_constr intern_body in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
   let prop = mkLambda (Name argname, argtyp, top_arity_let) in
   let def =
-    mkApp (Universes.constr_of_global (delayed_force fix_sub_ref),
+    mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
 	  [| argtyp ; wf_rel ;
-	     EConstr.Unsafe.to_constr (Evarutil.e_new_evar env evdref
-	       ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) (EConstr.of_constr wf_proof));
+	     Evarutil.e_new_evar env evdref
+	       ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
 	     prop |])
   in
-  let def = Typing.e_solve_evars env evdref (EConstr.of_constr def) in
-  let def = EConstr.Unsafe.to_constr def in
+  let def = Typing.e_solve_evars env evdref def in
   let _ = evdref := Evarutil.nf_evar_map !evdref in
   let def = mkApp (def, [|intern_body_lam|]) in
   let binders_rel = nf_evar_context !evdref binders_rel in
@@ -1057,21 +1063,22 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
       let hook l gr _ = 
-	let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
-	let ty = Term.it_mkProd_or_LetIn top_arity binders_rel in
+	let body = it_mkLambda_or_LetIn (mkApp (EConstr.of_constr (Universes.constr_of_global gr), [|make|])) binders_rel in
+	let ty = it_mkProd_or_LetIn top_arity binders_rel in
+	let ty = EConstr.Unsafe.to_constr ty in
 	let pl, univs = Evd.universe_context ?names:pl !evdref in
 	  (*FIXME poly? *)
-	let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
+	let ce = definition_entry ~poly ~types:ty ~univs (EConstr.Unsafe.to_constr (Evarutil.nf_evar !evdref body)) in
 	(** FIXME: include locality *)
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
 	  if Impargs.is_implicit_args () || not (List.is_empty impls) then
 	    Impargs.declare_manual_implicits false gr [impls]
       in
-      let typ = Term.it_mkProd_or_LetIn top_arity binders in
+      let typ = it_mkProd_or_LetIn top_arity binders in
 	hook, name, typ
     else 
-      let typ = Term.it_mkProd_or_LetIn top_arity binders_rel in
+      let typ = it_mkProd_or_LetIn top_arity binders_rel in
       let hook l gr _ = 
 	if Impargs.is_implicit_args () || not (List.is_empty impls) then
 	  Impargs.declare_manual_implicits false gr [impls]
@@ -1080,6 +1087,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let hook = Lemmas.mk_hook hook in
   let fullcoqc = Evarutil.nf_evar !evdref def in
   let fullctyp = Evarutil.nf_evar !evdref typ in
+  let fullcoqc = EConstr.Unsafe.to_constr fullcoqc in
+  let fullctyp = EConstr.Unsafe.to_constr fullctyp in
   Obligations.check_evars env !evdref;
   let evars, _, evars_def, evars_typ = 
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
@@ -1110,7 +1119,7 @@ let interp_recursive isfix fixl notations =
   let fixctximpenvs, fixctximps = List.split fiximppairs in
   let fixccls,fixcclimps = List.split (List.map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
-  let fixtypes = List.map (nf_evar !evdref) fixtypes in
+  let fixtypes = List.map (fun c -> EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.of_constr c))) fixtypes in
   let fiximps = List.map3
     (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps))
     fixctximps fixcclimps fixctxs in
@@ -1285,9 +1294,9 @@ let do_program_recursive local p fixkind fixl ntns =
   let collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
     let def =
-      nf_evar evd (EConstr.Unsafe.to_constr (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign))
+      EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign))
     and typ =
-      nf_evar evd (EConstr.Unsafe.to_constr (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign))
+      EConstr.Unsafe.to_constr (nf_evar evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign))
     in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ = 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 3c2fe46b3..851b87903 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -86,16 +86,18 @@ let rec contract3' env a b c = function
 let to_unsafe_judgment j = on_judgment EConstr.Unsafe.to_constr j
 
 let j_nf_betaiotaevar sigma j =
-  { uj_val = Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr j.uj_val);
-    uj_type = EConstr.Unsafe.to_constr (Reductionops.nf_betaiota sigma j.uj_type) }
+  { uj_val = Evarutil.nf_evar sigma j.uj_val;
+    uj_type = Reductionops.nf_betaiota sigma j.uj_type }
 
 let jv_nf_betaiotaevar sigma jl =
-  Array.map (fun j -> on_judgment EConstr.of_constr (j_nf_betaiotaevar sigma j)) jl
+  Array.map (fun j -> j_nf_betaiotaevar sigma j) jl
 
 (** Printers *)
 
 let pr_lconstr c = quote (pr_lconstr c)
 let pr_lconstr_env e s c = quote (pr_lconstr_env e s c)
+let pr_leconstr c = quote (pr_leconstr c)
+let pr_leconstr_env e s c = quote (pr_leconstr_env e s c)
 let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t)
 
 (** A canonisation procedure for constr such that comparing there
@@ -152,7 +154,8 @@ let explicit_flags =
     [print_implicits; print_coercions; print_no_symbol]; (** Then more! *)
     [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ]
 
-let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags
+let pr_explicit env sigma t1 t2 =
+  pr_explicit_aux env sigma (EConstr.to_constr sigma t1) (EConstr.to_constr sigma t2) explicit_flags
 
 let pr_db env i =
   try
@@ -263,9 +266,7 @@ let explain_number_branches env sigma cj expn =
   str "expects " ++  int expn ++ str " branches."
 
 let explain_ill_formed_branch env sigma c ci actty expty =
-  let actty = EConstr.Unsafe.to_constr actty in
-  let expty = EConstr.Unsafe.to_constr expty in
-  let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in
+  let simp t = Reductionops.nf_betaiota sigma (Evarutil.nf_evar sigma t) in
   let env = make_all_name_different env in
   let pc = pr_leconstr_env env sigma c in
   let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
@@ -302,13 +303,11 @@ let explain_unification_error env sigma p1 p2 = function
      | NotSameArgSize | NotSameHead | NoCanonicalStructure ->
         (* Error speaks from itself *) []
      | ConversionFailed (env,t1,t2) ->
-        let t1 = EConstr.to_constr sigma t1 in
-        let t2 = EConstr.to_constr sigma t2 in
-        if Term.eq_constr t1 p1 && Term.eq_constr t2 p2 then [] else
+        if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else
         let env = make_all_name_different env in
         let t1 = Evarutil.nf_evar sigma t1 in
         let t2 = Evarutil.nf_evar sigma t2 in
-        if not (Term.eq_constr t1 p1) || not (Term.eq_constr t2 p2) then
+        if not (EConstr.eq_constr sigma t1 p1) || not (EConstr.eq_constr sigma t2 p2) then
           let t1, t2 = pr_explicit env sigma t1 t2 in
           [str "cannot unify " ++ t1 ++ strbrk " and " ++ t2]
         else []
@@ -317,8 +316,6 @@ let explain_unification_error env sigma p1 p2 = function
 	strbrk " refers to a metavariable - please report your example" ++
         strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."]
      | InstanceNotSameType (evk,env,t,u) ->
-        let t = EConstr.to_constr sigma t in
-        let u = EConstr.to_constr sigma u in
         let t, u = pr_explicit env sigma t u in
         [str "unable to find a well-typed instantiation for " ++
         quote (pr_existential_key sigma evk) ++
@@ -331,11 +328,13 @@ let explain_unification_error env sigma p1 p2 = function
 	else
           [str "universe inconsistency"]
      | CannotSolveConstraint ((pb,env,t,u),e) ->
+        let t = EConstr.of_constr t in
+        let u = EConstr.of_constr u in
         let t = Evarutil.nf_evar sigma t in
         let u = Evarutil.nf_evar sigma u in
         let env = make_all_name_different env in
-        (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++
-        str " == " ++ pr_lconstr_env env sigma u)
+        (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++
+        str " == " ++ pr_leconstr_env env sigma u)
         :: aux t u e
      | ProblemBeyondCapabilities ->
         []
@@ -349,10 +348,9 @@ 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 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
+  let pc = pr_leconstr_env env sigma (Environ.j_val j) in
   let (pt, pct) = pr_explicit env sigma t (Environ.j_type j) in
   let ppreason = explain_unification_error env sigma j.uj_type t reason in
   pe ++
@@ -363,11 +361,9 @@ let explain_actual_type env sigma j t reason =
   ppreason ++ str ".")
 
 let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
-  let exptyp = EConstr.Unsafe.to_constr exptyp in
   let randl = jv_nf_betaiotaevar sigma randl in
   let exptyp = Evarutil.nf_evar sigma exptyp in
   let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
-  let actualtyp = EConstr.Unsafe.to_constr actualtyp in
   let rator = Evarutil.j_nf_evar sigma rator in
   let env = make_all_name_different env in
   let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in
@@ -520,11 +516,9 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
 
 let explain_ill_typed_rec_body env sigma i names vdefj vargs =
   let vdefj = Evarutil.jv_nf_evar sigma vdefj in
-  let vargs = Array.map EConstr.Unsafe.to_constr vargs in
-  let vdefj = Array.map to_unsafe_judgment vdefj in
   let vargs = Array.map (Evarutil.nf_evar sigma) vargs in
   let env = make_all_name_different env in
-  let pvd = pr_lconstr_env env sigma vdefj.(i).uj_val in
+  let pvd = pr_leconstr_env env sigma vdefj.(i).uj_val in
   let pvdt, pv = pr_explicit env sigma vdefj.(i).uj_type vargs.(i) in
   str "The " ++
   (match vdefj with [|_|] -> mt () | _ -> pr_nth (i+1) ++ spc ()) ++
@@ -584,13 +578,13 @@ let rec explain_evar_kind env sigma evk ty = function
   | Evar_kinds.SubEvar evk' ->
       let evi = Evd.find sigma evk' in
       let pc = match evi.evar_body with
-      | Evar_defined c -> pr_lconstr_env env sigma (Evarutil.nf_evar sigma c)
+      | Evar_defined c -> pr_leconstr_env env sigma (Evarutil.nf_evar sigma (EConstr.of_constr c))
       | Evar_empty -> assert false in
-      let ty' = Evarutil.nf_evar sigma evi.evar_concl in
+      let ty' = Evarutil.nf_evar sigma (EConstr.of_constr evi.evar_concl) in
       pr_existential_key sigma evk ++ str " of type " ++ ty ++
       str " in the partial instance " ++ pc ++
       str " found for " ++ explain_evar_kind env sigma evk'
-      (pr_lconstr_env env sigma ty') (snd evi.evar_source)
+      (pr_leconstr_env env sigma ty') (snd evi.evar_source)
 
 let explain_typeclass_resolution env sigma evi k =
   match Typeclasses.class_of_constr sigma (EConstr.of_constr evi.evar_concl) with
@@ -655,7 +649,7 @@ let explain_cannot_unify_local env sigma m n subn =
 
 let explain_refiner_cannot_generalize env sigma ty =
   str "Cannot find a well-typed generalisation of the goal with type: " ++
-  pr_lconstr_env env sigma ty ++ str "."
+  pr_leconstr_env env sigma ty ++ str "."
 
 let explain_no_occurrence_found env sigma c id =
   let c = EConstr.to_constr sigma c in
@@ -666,8 +660,8 @@ let explain_no_occurrence_found env sigma c id =
       | None -> str"the current goal") ++ str "."
 
 let explain_cannot_unify_binding_type env sigma m n =
-  let pm = pr_lconstr_env env sigma m in
-  let pn = pr_lconstr_env env sigma n in
+  let pm = pr_leconstr_env env sigma m in
+  let pn = pr_leconstr_env env sigma n in
   str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
   str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "."
 
@@ -760,8 +754,6 @@ let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1
     let ppreason = match e with
     | None -> mt()
     | Some (c1,c2,e) ->
-      let c1 = EConstr.to_constr sigma c1 in
-      let c2 = EConstr.to_constr sigma c2 in
       explain_unification_error env sigma c1 c2 (Some e)
     in
     str "Found incompatible occurrences of the pattern" ++ str ":" ++
@@ -841,12 +833,16 @@ let explain_pretype_error env sigma err =
     let actual = EConstr.Unsafe.to_constr actual in
     let expect = EConstr.Unsafe.to_constr expect in
     let env, actual, expect = contract2 env actual expect in
+    let actual = EConstr.of_constr actual in
+    let expect = EConstr.of_constr expect in
     explain_unexpected_type env sigma actual expect
   | NotProduct c -> explain_not_product env sigma c
   | CannotUnify (m,n,e) ->
     let m = EConstr.Unsafe.to_constr m in
     let n = EConstr.Unsafe.to_constr n in
     let env, m, n = contract2 env m n in
+    let m = EConstr.of_constr m in
+    let n = EConstr.of_constr n in
     explain_cannot_unify env sigma m n e
   | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn
   | CannotGeneralize ty -> explain_refiner_cannot_generalize env sigma ty
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 6da2f82ab..f4a786a73 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -818,7 +818,7 @@ let rec string_of_list sep f = function
 
 let solve_by_tac name evi t poly ctx =
   let id = name in
-  let concl = evi.evar_concl in
+  let concl = EConstr.of_constr evi.evar_concl in
   (* spiwack: the status is dropped. *)
   let (entry,_,ctx') = Pfedit.build_constant_by_tactic 
     id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
@@ -936,7 +936,7 @@ let rec solve_obligation prg num tac =
     Proof_global.make_terminator
       (obligation_terminator prg.prg_name num guard hook auto) in
   let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
-  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in
+  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in
   let _ = Pfedit.by !default_tactic in
   Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4376f51dc..cf3da7e02 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -59,7 +59,7 @@ let show_proof () =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   let p = Proof_global.give_me_the_proof () in
   let pprf = Proof.partial_proof p in
-  Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
+  Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf)
 
 let show_node () =
   (* spiwack: I'm have little clue what this function used to do. I deactivated it, 
@@ -459,7 +459,8 @@ let start_proof_and_print k l hook =
         let env = Evd.evar_filtered_env evi in
         try
           let concl = Evarutil.nf_evars_universes sigma evi.Evd.evar_concl in
-          if Evarutil.has_undefined_evars sigma (EConstr.of_constr concl) then raise Exit;
+          let concl = EConstr.of_constr concl in
+          if Evarutil.has_undefined_evars sigma concl then raise Exit;
           let c, _, ctx =
             Pfedit.build_by_tactic env (Evd.evar_universe_context sigma)
                                    concl (Tacticals.New.tclCOMPLETE tac)
@@ -877,6 +878,7 @@ let vernac_set_used_variables e =
   let env = Global.env () in
   let tys =
     List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in
+  let tys = List.map EConstr.Unsafe.to_constr tys in
   let l = Proof_using.process_expr env e tys in
   let vars = Environ.named_context env in
   List.iter (fun id -> 
@@ -1901,7 +1903,7 @@ let vernac_check_guard () =
     try
       let { Evd.it=gl ; sigma=sigma } = Proof.V82.top_goal pts in
       Inductiveops.control_only_guard (Goal.V82.env sigma gl)
-	pfterm;
+	(EConstr.Unsafe.to_constr pfterm);
       (str "The condition holds up to here")
     with UserError(_,s) ->
       (str ("Condition violated: ") ++s)