Evarconv API using EConstr.

26 files changed, 255 insertions, 275 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 05f98a41f..62627a416 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -148,21 +148,11 @@ let nf_evar_map_undefined evm =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
-(* A probably faster though more approximative variant of
-   [has_undefined (nf_evar c)]: instances are not substituted and
-   maybe an evar occurs in an instance and it would disappear by
-   instantiation *)
-
 let has_undefined_evars evd t =
   let rec has_ev t =
-    match kind_of_term t with
-    | Evar (ev,args) ->
-        (match evar_body (Evd.find evd ev) with
-        | Evar_defined c ->
-            has_ev c; Array.iter has_ev args
-        | Evar_empty ->
-	    raise NotInstantiatedEvar)
-    | _ -> iter_constr has_ev t in
+    match EConstr.kind evd t with
+    | Evar _ -> raise NotInstantiatedEvar
+    | _ -> EConstr.iter evd has_ev t in
   try let _ = has_ev t in false
   with (Not_found | NotInstantiatedEvar) -> true
 
@@ -171,10 +161,10 @@ let is_ground_term evd t =
 
 let is_ground_env evd env =
   let is_ground_rel_decl = function
-    | RelDecl.LocalDef (_,b,_) -> is_ground_term evd b
+    | RelDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b)
     | _ -> true in
   let is_ground_named_decl = function
-    | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd b
+    | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b)
     | _ -> true in
   List.for_all is_ground_rel_decl (rel_context env) &&
   List.for_all is_ground_named_decl (named_context env)
@@ -208,27 +198,18 @@ let head_evar =
    guess it should consider Case too) *)
 
 let whd_head_evar_stack sigma c =
-  let rec whrec (c, l as s) =
-    match kind_of_term c with
-      | Evar (evk,args as ev) ->
-        let v =
-          try Some (existential_value sigma ev)
-          with NotInstantiatedEvar | Not_found  -> None in
-        begin match v with
-        | None -> s
-        | Some c -> whrec (c, l)
-        end
+  let rec whrec (c, l) =
+    match EConstr.kind sigma c with
       | Cast (c,_,_) -> whrec (c, l)
       | App (f,args) -> whrec (f, args :: l)
-      | _ -> s
+      | c -> (EConstr.of_kind c, l)
   in
   whrec (c, [])
 
 let whd_head_evar sigma c =
+  let open EConstr in
   let (f, args) = whd_head_evar_stack sigma c in
-  (** optim: don't reallocate if empty/singleton *)
   match args with
-  | [] -> f
   | [arg] -> mkApp (f, arg)
   | _ -> mkApp (f, Array.concat args)
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index a2e2a07dd..d6e2d4534 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -91,12 +91,12 @@ exception NoHeadEvar
 val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
 
 (* Expand head evar if any *)
-val whd_head_evar :  evar_map -> constr -> constr
+val whd_head_evar :  evar_map -> EConstr.constr -> EConstr.constr
 
 (* An over-approximation of [has_undefined (nf_evars evd c)] *)
-val has_undefined_evars : evar_map -> constr -> bool
+val has_undefined_evars : evar_map -> EConstr.constr -> bool
 
-val is_ground_term :  evar_map -> constr -> bool
+val is_ground_term :  evar_map -> EConstr.constr -> bool
 val is_ground_env  :  evar_map -> env -> bool
 
 (** [gather_dependent_evars evm seeds] classifies the evars in [evm]
diff --git a/engine/termops.ml b/engine/termops.ml
index 356312e2f..26b22be4e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1068,6 +1068,17 @@ let dependency_closure env sigma sign hyps =
         sign in
     List.rev lh
 
+let global_app_of_constr sigma c =
+  let open Univ in
+  let open Globnames in
+  match EConstr.kind sigma c with
+  | Const (c, u) -> (ConstRef c, u), None
+  | Ind (i, u) -> (IndRef i, u), None
+  | Construct (c, u) -> (ConstructRef c, u), None
+  | Var id -> (VarRef id, Instance.empty), None
+  | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
+  | _ -> raise Not_found
+
 (* Combinators on judgments *)
 
 let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
diff --git a/engine/termops.mli b/engine/termops.mli
index b536b0fb8..24c2c82f2 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -254,6 +254,7 @@ val clear_named_body : Id.t -> env -> env
 
 val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list
 val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t
+val global_app_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses * EConstr.constr option
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 6720fcef8..51a113219 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -446,15 +446,6 @@ let global_of_constr c =
   | Var id -> VarRef id, Instance.empty
   | _ -> raise Not_found
 
-let global_app_of_constr c =
-  match kind_of_term c with
-  | Const (c, u) -> (ConstRef c, u), None
-  | Ind (i, u) -> (IndRef i, u), None
-  | Construct (c, u) -> (ConstructRef c, u), None
-  | Var id -> (VarRef id, Instance.empty), None
-  | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
-  | _ -> raise Not_found
-
 open Declarations
 
 let type_of_reference env r =
diff --git a/engine/universes.mli b/engine/universes.mli
index 725c21d29..c3e2055f3 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -130,8 +130,6 @@ val fresh_universe_context_set_instance : universe_context_set ->
 (** Raises [Not_found] if not a global reference. *)
 val global_of_constr : constr -> Globnames.global_reference puniverses
 
-val global_app_of_constr : constr -> Globnames.global_reference puniverses * constr option
-
 val constr_of_global_univ : Globnames.global_reference puniverses -> constr
 
 val extend_context : 'a in_universe_context_set -> universe_context_set -> 
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 80307ce8e..076e4c05e 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -454,7 +454,7 @@ let evd_convertible env evd x y =
        unsolvable constraints remain, so we check that this unification
        does not introduce any new problem. *)
     let _, pbs = Evd.extract_all_conv_pbs evd in
-    let evd' = Evarconv.the_conv_x env x y evd in
+    let evd' = Evarconv.the_conv_x env (EConstr.of_constr x) (EConstr.of_constr y) evd in
     let _, pbs' = Evd.extract_all_conv_pbs evd' in
     if evd' == evd || problem_inclusion pbs' pbs then Some evd'
     else None
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 258ee5ad6..340dd2c28 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -237,7 +237,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
       failwith "NoChange";
     end
   in
-  let eq_constr = Evarconv.e_conv env (ref sigma) in
+  let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) (EConstr.of_constr c1) (EConstr.of_constr c2) in
   if not (noccurn 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp t) then nochange "not an equality";
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index cc39b7260..e0d99d453 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -298,9 +298,9 @@ let unif_EQ_args env sigma pa a =
   prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a 
 ;;
 
-let unif_HO env ise p c = Evarconv.the_conv_x env p c ise
+let unif_HO env ise p c = Evarconv.the_conv_x env (EConstr.of_constr p) (EConstr.of_constr c) ise
 
-let unif_HOtype env ise p c = Evarconv.the_conv_x_leq env p c ise
+let unif_HOtype env ise p c = Evarconv.the_conv_x_leq env (EConstr.of_constr p) (EConstr.of_constr c) ise
 
 let unif_HO_args env ise0 pa i ca =
   let n = Array.length pa in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a68daf4e5..04f50d50e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -78,9 +78,6 @@ let list_try_compile f l =
 let force_name =
   let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na
 
-let to_conv_fun f = (); fun env sigma pb c1 c2 ->
-  f env sigma pb (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2)
-
 (************************************************************************)
 (*            Pattern-matching compilation (Cases)                      *)
 (************************************************************************)
@@ -311,7 +308,7 @@ let inh_coerce_to_ind evdref env loc ty tyi =
      constructor and renounce if not able to give more information *)
   (* devrait être indifférent d'exiger leq ou pas puisque pour
      un inductif cela doit être égal *)
-  if not (e_cumul env evdref expected_typ ty) then evdref := sigma
+  if not (e_cumul env evdref (EConstr.of_constr expected_typ) (EConstr.of_constr ty)) then evdref := sigma
 
 let binding_vars_of_inductive = function
   | NotInd _ -> []
@@ -395,7 +392,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 	    let current =
 	      if List.is_empty deps && isEvar typ then
 	      (* Don't insert coercions if dependent; only solve evars *)
-		let _ = e_cumul pb.env pb.evdref indt typ in
+		let _ = e_cumul pb.env pb.evdref (EConstr.of_constr indt) (EConstr.of_constr typ) in
 		current
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env)
@@ -1639,7 +1636,7 @@ let abstract_tycon loc env evdref subst tycon extenv t =
               1 (rel_context env) in
         let ev' = e_new_evar env evdref ~src ty in
         let ev = (fst ev, Array.map EConstr.of_constr (snd ev)) in
-        begin match solve_simple_eqn (to_conv_fun (evar_conv_x full_transparent_state)) env !evdref (None,ev,EConstr.of_constr (substl inst ev')) with
+        begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,EConstr.of_constr (substl inst ev')) with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
         end;
@@ -1690,7 +1687,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
         let evd,tt = Typing.type_of extenv !evdref t in
         evdref := evd;
         (t,tt) in
-  let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
+  let b = e_cumul env evdref (EConstr.of_constr tt) (EConstr.mkSort s) (* side effect *) in
   if not b then anomaly (Pp.str "Build_tycon: should be a type");
   { uj_val = t; uj_type = tt }
 
@@ -2083,7 +2080,7 @@ let constr_of_pat env evdref arsign pat avoid =
 		  try
 		    let env = push_rel_context sign env in
 		    evdref := the_conv_x_leq (push_rel_context sign env)
-		      (lift (succ m) ty) (lift 1 apptype) !evdref;
+		      (EConstr.of_constr (lift (succ m) ty)) (EConstr.of_constr (lift 1 apptype)) !evdref;
 		    let eq_t = mk_eq evdref (lift (succ m) ty)
 		      (mkRel 1) (* alias *)
 		      (lift 1 app) (* aliased term *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c5418d22e..0ea6758a7 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -65,7 +65,7 @@ let apply_coercion_args env evd check isproj argl funj =
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
       match kind_of_term (whd_all env evd (EConstr.of_constr typ)) with
       | Prod (_,c1,c2) ->
-        if check && not (e_cumul env evdref (Retyping.get_type_of env evd (EConstr.of_constr h)) c1) then
+        if check && not (e_cumul env evdref (EConstr.of_constr (Retyping.get_type_of env evd (EConstr.of_constr h))) (EConstr.of_constr c1)) then
 	  raise NoCoercion;
         apply_rec (h::acc) (subst1 h c2) restl
       | _ -> anomaly (Pp.str "apply_coercion_args")
@@ -147,7 +147,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
   let rec coerce_unify env x y =
     let x = hnf env !evdref (EConstr.of_constr x) and y = hnf env !evdref (EConstr.of_constr y) in
       try
-	evdref := the_conv_x_leq env x y !evdref;
+	evdref := the_conv_x_leq env (EConstr.of_constr x) (EConstr.of_constr y) !evdref;
 	None
       with UnableToUnify _ -> coerce' env x y
   and coerce' env x y : (Term.constr -> Term.constr) option =
@@ -162,7 +162,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
       let rec aux tele typ typ' i co =
 	if i < len then
 	  let hdx = l.(i) and hdy = l'.(i) in
-	    try evdref := the_conv_x_leq env hdx hdy !evdref;
+	    try evdref := the_conv_x_leq env (EConstr.of_constr hdx) (EConstr.of_constr hdy) !evdref;
 	      let (n, eqT), restT = dest_prod typ in
 	      let (n', eqT'), restT' = dest_prod typ' in
 		aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
@@ -170,7 +170,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 	      let (n, eqT), restT = dest_prod typ in
 	      let (n', eqT'), restT' = dest_prod typ' in
 	      let _ =
-		try evdref := the_conv_x_leq env eqT eqT' !evdref
+		try evdref := the_conv_x_leq env (EConstr.of_constr eqT) (EConstr.of_constr eqT') !evdref
 		with UnableToUnify _ -> raise NoSubtacCoercion
 	      in
 		(* Disallow equalities on arities *)
@@ -458,11 +458,11 @@ let inh_coerce_to_fail env evd rigidonly v t c1 =
 	  | None -> evd, None, t
       with Not_found -> raise NoCoercion
     in
-      try (the_conv_x_leq env t' c1 evd, v')
+      try (the_conv_x_leq env (EConstr.of_constr t') (EConstr.of_constr c1) evd, v')
       with UnableToUnify _ -> raise NoCoercion
 
 let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
-  try (the_conv_x_leq env t c1 evd, v)
+  try (the_conv_x_leq env (EConstr.of_constr t) (EConstr.of_constr c1) evd, v)
   with UnableToUnify (best_failed_evd,e) ->
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 8f3f671ab..c8dcb19b4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -30,7 +30,7 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 type unify_fun = transparent_state ->
-  env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
+  env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
 
 let debug_unification = ref (false)
 let _ = Goptions.declare_bool_option {
@@ -42,33 +42,32 @@ let _ = Goptions.declare_bool_option {
   Goptions.optwrite = (fun a -> debug_unification:=a);
 }
 
-let to_conv_fun f = (); fun env sigma pb c1 c2 ->
-  f env sigma pb (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2)
-
 let unfold_projection env evd ts p c =
+  let open EConstr in
   let cst = Projection.constant p in
     if is_transparent_constant ts cst then
       Some (mkProj (Projection.make cst true, c))
     else None
       
 let eval_flexible_term ts env evd c =
-  match kind_of_term c with
+  let open EConstr in
+  match EConstr.kind evd c with
   | Const (c,u as cu) ->
       if is_transparent_constant ts c
-      then constant_opt_value_in env cu
+      then Option.map EConstr.of_constr (constant_opt_value_in env cu)
       else None
   | Rel n ->
       (try match lookup_rel n env with
            | RelDecl.LocalAssum _ -> None
-           | RelDecl.LocalDef (_,v,_) -> Some (lift n v)
+           | RelDecl.LocalDef (_,v,_) -> Some (Vars.lift n (EConstr.of_constr v))
        with Not_found -> None)
   | Var id ->
       (try
 	 if is_transparent_variable ts id then
-	   env |> lookup_named id |> NamedDecl.get_value
+	   Option.map EConstr.of_constr (env |> lookup_named id |> NamedDecl.get_value)
 	 else None
        with Not_found -> None)
-  | LetIn (_,b,_,c) -> Some (subst1 b c)
+  | LetIn (_,b,_,c) -> Some (Vars.subst1 b c)
   | Lambda _ -> Some c
   | Proj (p, c) -> 
     if Projection.unfolded p then assert false
@@ -77,12 +76,11 @@ let eval_flexible_term ts env evd c =
 
 type flex_kind_of_term =
   | Rigid
-  | MaybeFlexible of Constr.t (* reducible but not necessarily reduced *)
-  | Flexible of existential
+  | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *)
+  | Flexible of EConstr.existential
 
 let flex_kind_of_term ts env evd c sk =
-  let c = EConstr.Unsafe.to_constr c in
-  match kind_of_term c with
+  match EConstr.kind evd c with
     | LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
       Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c)
     | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c
@@ -92,12 +90,13 @@ let flex_kind_of_term ts env evd c sk =
     | Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
     | Cast _ | App _ | Case _ -> assert false
 
-let zip evd (c, stk) = EConstr.Unsafe.to_constr (Stack.zip evd (c, stk))
+let add_conv_pb (pb, env, x, y) sigma =
+  Evd.add_conv_pb (pb, env, EConstr.Unsafe.to_constr x, EConstr.Unsafe.to_constr y) sigma
 
 let apprec_nohdbeta ts env evd c =
-  let (t,sk as appr) = Reductionops.whd_nored_state evd (EConstr.of_constr c, []) in
+  let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
   if Stack.not_purely_applicative sk
-  then zip evd (fst (whd_betaiota_deltazeta_for_iota_state
+  then Stack.zip evd (fst (whd_betaiota_deltazeta_for_iota_state
 		   ts env evd Cst_stack.empty appr))
   else c
 
@@ -106,8 +105,9 @@ let position_problem l2r = function
   | CUMUL -> Some l2r
 
 let occur_rigidly (evk,_ as ev) evd t =
+  let open EConstr in
   let rec aux t =
-    match kind_of_term (whd_evar evd t) with
+    match EConstr.kind evd t with
     | App (f, c) -> if aux f then Array.exists aux c else false
     | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true
     | Proj (p, c) -> not (aux c)
@@ -117,7 +117,7 @@ let occur_rigidly (evk,_ as ev) evd t =
     | Const _ -> false
     | Prod (_, b, t) -> ignore(aux b || aux t); true
     | Rel _ | Var _ -> false
-    | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false
+    | Case (_,_,c,_) -> if eq_constr evd (mkEvar ev) c then raise Occur else false
   in try ignore(aux t); false with Occur -> true
 
 (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose 
@@ -141,23 +141,22 @@ let occur_rigidly (evk,_ as ev) evd t =
    projection would have been reduced) *)
 
 let check_conv_record env sigma (t1,sk1) (t2,sk2) =
-  let t1 = EConstr.Unsafe.to_constr t1 in
-  let t2 = EConstr.Unsafe.to_constr t2 in
-  let (proji, u), arg = Universes.global_app_of_constr t1 in
+  let open EConstr in
+  let (proji, u), arg = Termops.global_app_of_constr sigma t1 in
   let canon_s,sk2_effective =
     try
-      match kind_of_term t2 with
+      match EConstr.kind sigma t2 with
 	Prod (_,a,b) -> (* assert (l2=[]); *)
-	  let _, a, b = destProd (Evarutil.nf_evar sigma t2) in
-          if EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) then
+	  let _, a, b = destProd sigma t2 in
+          if Vars.noccurn sigma 1 b then
             lookup_canonical_conversion (proji, Prod_cs),
-	    (Stack.append_app [|EConstr.of_constr a;EConstr.of_constr (pop (EConstr.of_constr b))|] Stack.empty)
+	    (Stack.append_app [|a;EConstr.of_constr (pop b)|] Stack.empty)
           else raise Not_found
       | Sort s ->
 	lookup_canonical_conversion
 	  (proji, Sort_cs (family_of_sort s)),[]
       | _ ->
-	let c2 = global_of_constr t2 in
+	let c2 = global_of_constr (EConstr.to_constr sigma t2) in
 	  lookup_canonical_conversion (proji, Const_cs c2),sk2
     with Not_found ->
       let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in 
@@ -165,17 +164,19 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
   in
   let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
         o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
+  let us = List.map EConstr.of_constr us in
+  let params = List.map EConstr.of_constr params in
   let params1, c1, extra_args1 =
     match arg with
     | Some c -> (* A primitive projection applied to c *)
-      let ty = Retyping.get_type_of ~lax:true env sigma (EConstr.of_constr c) in
+      let ty = Retyping.get_type_of ~lax:true env sigma c in
       let (i,u), ind_args = 
 	try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty)
 	with _ -> raise Not_found
       in Stack.append_app_list (List.map EConstr.of_constr ind_args) Stack.empty, c, sk1
     | None ->
       match Stack.strip_n_app nparams sk1 with
-      | Some (params1, c1, extra_args1) -> params1, EConstr.Unsafe.to_constr c1, extra_args1
+      | Some (params1, c1, extra_args1) -> params1, c1, extra_args1
       | _ -> raise Not_found in
   let us2,extra_args2 =
     let l_us = List.length us in
@@ -184,13 +185,13 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
       | None -> raise Not_found
       | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
   let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
-  let c' = subst_univs_level_constr subst c in
+  let c' = EConstr.of_constr (subst_univs_level_constr subst c) in
   let t' = subst_univs_level_constr subst t' in
-  let bs' = List.map (subst_univs_level_constr subst) bs in
+  let bs' = List.map (subst_univs_level_constr subst %> EConstr.of_constr) bs in
   let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in
-    ctx',(h, t2),c',bs',(Stack.append_app_list (List.map EConstr.of_constr params) Stack.empty,params1),
-    (Stack.append_app_list (List.map EConstr.of_constr us) Stack.empty,us2),(extra_args1,extra_args2),c1,
-    (n, zip sigma (EConstr.of_constr t2,sk2))
+    ctx',(EConstr.of_constr h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
+    (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
+    (n, Stack.zip sigma (t2,sk2))
 
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
@@ -220,11 +221,10 @@ let ise_exact ise x1 x2 =
   | Some _, Success i -> UnifFailure (i,NotSameArgSize)
 
 let ise_array2 evd f v1 v2 =
-  let inj c = EConstr.Unsafe.to_constr c in
   let rec allrec i = function
     | -1 -> Success i
     | n ->
-        match f i (inj v1.(n)) (inj v2.(n)) with
+        match f i v1.(n) v2.(n) with
 	| Success i' -> allrec i' (n-1)
 	| UnifFailure _ as x -> x in
   let lv1 = Array.length v1 in
@@ -234,14 +234,13 @@ let ise_array2 evd f v1 v2 =
 (* Applicative node of stack are read from the outermost to the innermost
    but are unified the other way. *)
 let rec ise_app_stack2 env f evd sk1 sk2 =
-  let inj = EConstr.Unsafe.to_constr in
   match sk1,sk2 with
   | Stack.App node1 :: q1, Stack.App node2 :: q2 ->
      let (t1,l1) = Stack.decomp_node_last node1 q1 in
      let (t2,l2) = Stack.decomp_node_last node2 q2 in
      begin match ise_app_stack2 env f evd l1 l2 with
 	   |(_,UnifFailure _) as x -> x
-	   |x,Success i' -> x,f env i' CONV (inj t1) (inj t2)
+	   |x,Success i' -> x,f env i' CONV t1 t2
      end
   | _, _ -> (sk1,sk2), Success evd
 
@@ -255,14 +254,13 @@ let push_rec_types pfix env =
    stacks but not the entire stacks, the first part of the answer is
    Some(the remaining prefixes to tackle)) *)
 let ise_stack2 no_app env evd f sk1 sk2 =
-  let inj = EConstr.Unsafe.to_constr in
   let rec ise_stack2 deep i sk1 sk2 =
     let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i
       else None, x in
     match sk1, sk2 with
     | [], [] -> None, Success i
     | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 ->
-      (match f env i CONV (inj t1) (inj t2) with
+      (match f env i CONV t1 t2 with
       | Success i' ->
 	(match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with
 	| Success i'' -> ise_stack2 true i'' q1 q2
@@ -295,7 +293,6 @@ let ise_stack2 no_app env evd f sk1 sk2 =
 
 (* Make sure that the matching suffix is the all stack *)
 let exact_ise_stack2 env evd f sk1 sk2 =
-  let inj = EConstr.Unsafe.to_constr in
   let rec ise_stack2 i sk1 sk2 =
     match sk1, sk2 with
     | [], [] -> Success i
@@ -303,7 +300,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
       ise_and i [
       (fun i -> ise_stack2 i q1 q2);
       (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);
-      (fun i -> f env i CONV (inj t1) (inj t2))]
+      (fun i -> f env i CONV t1 t2)]
     | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
       Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
       if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
@@ -341,10 +338,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
       let e =
 	try
 	  let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
-	    env evd term1 term2 
+	    env evd (EConstr.Unsafe.to_constr term1) (EConstr.Unsafe.to_constr term2)
 	  in
 	    if b then Success evd
-	    else UnifFailure (evd, ConversionFailed (env,EConstr.of_constr term1,EConstr.of_constr term2))
+	    else UnifFailure (evd, ConversionFailed (env,term1,term2))
 	with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
       in
 	match e with
@@ -361,19 +358,19 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
         let term2 = apprec_nohdbeta (fst ts) env evd term2 in
 	let default () = 
           evar_eqappr_x ts env evd pbty
-            (whd_nored_state evd (EConstr.of_constr term1,Stack.empty), Cst_stack.empty)
-            (whd_nored_state evd (EConstr.of_constr term2,Stack.empty), Cst_stack.empty)
+            (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
+            (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
 	in
-          begin match EConstr.kind evd (EConstr.of_constr term1), EConstr.kind evd (EConstr.of_constr term2) with
+          begin match EConstr.kind evd term1, EConstr.kind evd term2 with
           | Evar ev, _ when Evd.is_undefined evd (fst ev) ->
-            (match solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd
-              (position_problem true pbty,ev, EConstr.of_constr term2) with
+            (match solve_simple_eqn (evar_conv_x ts) env evd
+              (position_problem true pbty,ev, term2) with
 	      | UnifFailure (_,OccurCheck _) -> 
 		(* Eta-expansion might apply *) default ()
 	      | x -> x)
           | _, Evar ev when Evd.is_undefined evd (fst ev) ->
-            (match solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd
-              (position_problem false pbty,ev, EConstr.of_constr term1) with
+            (match solve_simple_eqn (evar_conv_x ts) env evd
+              (position_problem false pbty,ev, term1) with
 	      | UnifFailure (_, OccurCheck _) ->
 		(* Eta-expansion might apply *) default () 
 	      | x -> x)
@@ -382,6 +379,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
 
 and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
+  let open EConstr in
   let quick_fail i = (* not costly, loses info *)
     UnifFailure (i, NotSameHead)
   in
@@ -391,28 +389,27 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       | Some l1' -> (* Miller-Pfenning's patterns unification *)
 	let t2 = EConstr.of_constr (nf_evar evd (EConstr.Unsafe.to_constr tM)) (** FIXME *) in
 	let t2 = solve_pattern_eqn env evd l1' t2 in
-	  solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env evd
-	    (position_problem on_left pbty,ev, EConstr.of_constr t2) 
+	  solve_simple_eqn (evar_conv_x ts) env evd
+	    (position_problem on_left pbty,ev,EConstr.of_constr t2) 
   in
   let consume_stack on_left (termF,skF) (termO,skO) evd =
-    let inj = EConstr.Unsafe.to_constr in
     let switch f a b = if on_left then f a b else f b a in
     let not_only_app = Stack.not_purely_applicative skO in
     match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with
       |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
-	switch (evar_conv_x ts env i' pbty) (zip evd (termF,l)) (zip evd (termO,r))
+	switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
       |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
-	switch (evar_conv_x ts env i' pbty) (zip evd (termF,l)) (zip evd (termO,r))
-      |None, Success i' -> switch (evar_conv_x ts env i' pbty) (inj termF) (inj termO)
+	switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
+      |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO
       |_, (UnifFailure _ as x) -> x
       |Some _, _ -> UnifFailure (evd,NotSameArgSize) in
   let eta env evd onleft sk term sk' term' =
     assert (match sk with [] -> true | _ -> false);
-    let (na,c1,c'1) = destLambda term in
-    let c = nf_evar evd c1 in
+    let (na,c1,c'1) = destLambda evd term in
+    let c = EConstr.to_constr evd c1 in
     let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
-      (fst ts) env' evd Cst_stack.empty (EConstr.of_constr c'1, Stack.empty) in
+      (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
     let out2 = whd_nored_state evd
       (Stack.zip evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), 
       Cst_stack.empty in
@@ -438,12 +435,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       match Stack.list_of_app_stack skF with
       | None -> quick_fail evd
       | Some lF -> 
-        let tM = zip evd apprM in
+        let tM = Stack.zip evd apprM in
 	  miller_pfenning on_left
 	    (fun () -> if not_only_app then (* Postpone the use of an heuristic *)
-	      switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (zip evd apprF) tM
+	      switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
 	    else quick_fail i)
-	  ev lF (EConstr.of_constr tM) i
+	  ev lF tM i
     and consume (termF,skF as apprF) (termM,skM as apprM) i = 
       if not (Stack.is_empty skF && Stack.is_empty skM) then
         consume_stack on_left apprF apprM i
@@ -487,7 +484,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let eta evd =
       match EConstr.kind evd termR with
       | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR ->
-         eta env evd false skR (EConstr.Unsafe.to_constr termR) skF termF
+         eta env evd false skR termR skF termF
       | Construct u -> eta_constructor ts env evd skR u skF termF
       | _ -> UnifFailure (evd,NotSameHead)
     in
@@ -495,7 +492,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     | None ->
         ise_try evd [consume_stack on_left apprF apprR; eta]
     | Some lF ->
-        let tR = zip evd apprR in
+        let tR = Stack.zip evd apprR in
 	  miller_pfenning on_left
 	    (fun () ->
 	      ise_try evd 
@@ -503,17 +500,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 		 (fun i -> 
 		   if not (occur_rigidly ev i tR) then
                      let i,tF =
-                       if isRel tR || isVar tR then
+                       if isRel i tR || isVar i tR then
                          (* Optimization so as to generate candidates *)
-                         let i,ev = evar_absorb_arguments env i (fst ev, Array.map EConstr.of_constr (snd ev)) lF in
+                         let i,ev = evar_absorb_arguments env i ev lF in
                          i,mkEvar ev
                        else
-                         i,zip evd apprF in
+                         i,Stack.zip evd apprF in
 		     switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
 	               tF tR
 		   else
-                     UnifFailure (evd,OccurCheck (fst ev,EConstr.of_constr tR)))])
-	    (fst ev, Array.map EConstr.of_constr (snd ev)) lF (EConstr.of_constr tR) evd
+                     UnifFailure (evd,OccurCheck (fst ev,tR)))])
+	    ev lF tR evd
   in
   let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
   (* Evar must be undefined since we have flushed evars *)
@@ -531,20 +528,20 @@ 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' (mkEvar ev1)) in
-	      if EConstr.isEvar i' ev1' then
-		solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i'
-		  (position_problem true pbty,EConstr.destEvar i' ev1', term2)
+	    let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (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)
 	      else 
 		evar_eqappr_x ts env evd pbty 
 		  ((ev1', sk1), csts1) ((term2, sk2), csts2)
 	  | 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' (mkEvar ev2)) in
-	      if EConstr.isEvar i' ev2' then
-		solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i'
-		  (position_problem false pbty,EConstr.destEvar i' ev2',Stack.zip evd (term1,r))
+	    let ev2' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (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))
 	      else 
 		evar_eqappr_x ts env evd pbty 
 		  ((ev2', sk1), csts1) ((term2, sk2), csts2)
@@ -552,10 +549,10 @@ 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' (mkEvar ev1)) in
-	      if EConstr.isEvar i' ev1' then
-		solve_simple_eqn (to_conv_fun (evar_conv_x ts)) env i'
-	          (position_problem true pbty,EConstr.destEvar i' ev1',Stack.zip evd (term2,r))
+	    let ev1' = EConstr.of_constr (whd_evar i' (EConstr.Unsafe.to_constr (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))
 	      else evar_eqappr_x ts env evd pbty 
 		((ev1', sk1), csts1) ((term2, sk2), csts2)
 	  | None, (UnifFailure _ as x) ->
@@ -592,9 +589,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
           if Evar.equal sp1 sp2 then
 	    match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
 	    |None, Success i' ->
-              Success (solve_refl (to_conv_fun (fun env i pbty a1 a2 ->
-                is_success (evar_conv_x ts env i pbty a1 a2)))
-                env i' (position_problem true pbty) sp1 (Array.map EConstr.of_constr al1) (Array.map EConstr.of_constr al2))
+              Success (solve_refl (fun env i pbty a1 a2 ->
+                is_success (evar_conv_x ts env i pbty a1 a2))
+                env i' (position_problem true pbty) sp1 al1 al2)
 	    |_, (UnifFailure _ as x) -> x
             |Some _, _ -> UnifFailure (i,NotSameArgSize)
           else UnifFailure (i,NotSameHead)
@@ -602,13 +599,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	ise_try evd [f1; f2]
 
     | Flexible ev1, MaybeFlexible v2 ->
-      flex_maybeflex true (fst ev1, Array.map EConstr.of_constr (snd ev1)) (appr1,csts1) (appr2,csts2) (EConstr.of_constr v2)
+      flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2
 
     | MaybeFlexible v1, Flexible ev2 -> 
-      flex_maybeflex false (fst ev2, Array.map EConstr.of_constr (snd ev2)) (appr2,csts2) (appr1,csts1) (EConstr.of_constr v1)
+      flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1
 
     | MaybeFlexible v1, MaybeFlexible v2 -> begin
-        match kind_of_term (EConstr.Unsafe.to_constr term1), kind_of_term (EConstr.Unsafe.to_constr term2) with
+        match EConstr.kind evd term1, EConstr.kind evd term2 with
         | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
         let f1 i = (* FO *)
           ise_and i
@@ -617,14 +614,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                 (fun i -> evar_conv_x ts env i CUMUL t2 t1)]);
              (fun i -> evar_conv_x ts env i CONV b1 b2);
 	     (fun i ->
-	       let b = nf_evar i b1 in
-	       let t = nf_evar i t1 in
+	       let b = EConstr.to_constr i b1 in
+	       let t = EConstr.to_constr i t1 in
                let na = Nameops.name_max na1 na2 in
 	       evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	and f2 i =
-          let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (EConstr.of_constr v1,sk1)
-          and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (EConstr.of_constr v2,sk2)
+          let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
+          and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2)
 	  in evar_eqappr_x ts env i pbty out1 out2
 	in
 	ise_try evd [f1; f2]
@@ -636,8 +633,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    [(fun i -> evar_conv_x ts env i CONV c c');
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	  and f2 i =
-            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (EConstr.of_constr v1,sk1)
-            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (EConstr.of_constr v2,sk2)
+            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
+            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2)
 	    in evar_eqappr_x ts env i pbty out1 out2
 	  in
 	    ise_try evd [f1; f2]
@@ -645,7 +642,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	(* Catch the p.c ~= p c' cases *)
 	| Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' ->
 	  let res = 
-	    try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p (EConstr.of_constr c) [])))
+	    try Some (destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p c [])))
 	    with Retyping.RetypeError _ -> None
 	  in
 	    (match res with 
@@ -656,7 +653,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	      
 	| Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') ->
 	  let res = 
-	    try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' (EConstr.of_constr c') [])))
+	    try Some (destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' c' [])))
 	    with Retyping.RetypeError _ -> None
 	  in 
 	    (match res with
@@ -710,7 +707,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    let applicative_stack = fst (Stack.strip_app sk2) in
 	    is_unnamed
 	      (fst (whd_betaiota_deltazeta_for_iota_state
-		      (fst ts) env i Cst_stack.empty (EConstr.of_constr v2, applicative_stack))) in
+		      (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in
           let rhs_is_already_stuck =
             rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
 
@@ -718,12 +715,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    && (not (Stack.not_purely_applicative sk1)) then
 	    evar_eqappr_x ~rhs_is_already_stuck ts env i pbty
 	      (whd_betaiota_deltazeta_for_iota_state
-		 (fst ts) env i (Cst_stack.add_cst term1 csts1) (EConstr.of_constr v1,sk1))
+		 (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
 	      (appr2,csts2)
 	  else
 	    evar_eqappr_x ts env i pbty (appr1,csts1)
 	      (whd_betaiota_deltazeta_for_iota_state
-		 (fst ts) env i (Cst_stack.add_cst term2 csts2) (EConstr.of_constr v2,sk2))
+		 (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
 	in
 	ise_try evd [f1; f2; f3]
     end
@@ -731,14 +728,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 ->
         let (na1,c1,c'1) = EConstr.destLambda evd term1 in
         let (na2,c2,c'2) = EConstr.destLambda evd term2 in
-        let inj = EConstr.Unsafe.to_constr in
         assert app_empty;
         ise_and evd
-          [(fun i -> evar_conv_x ts env i CONV (inj c1) (inj c2));
+          [(fun i -> evar_conv_x ts env i CONV c1 c2);
            (fun i ->
-	     let c = nf_evar i (inj c1) in
+	     let c = EConstr.to_constr i c1 in
              let na = Nameops.name_max na1 na2 in
-	     evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV (inj c'1) (inj c'2))]
+	     evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]
 
     | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
     | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1
@@ -752,7 +748,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	and f4 i =
 	  evar_eqappr_x ts env i pbty
 	    (whd_betaiota_deltazeta_for_iota_state
-	       (fst ts) env i (Cst_stack.add_cst term1 csts1) (EConstr.of_constr v1,sk1))
+	       (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
 	    (appr2,csts2)
 	in
 	  ise_try evd [f3; f4]
@@ -766,19 +762,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	and f4 i =
 	  evar_eqappr_x ts env i pbty (appr1,csts1)
 	    (whd_betaiota_deltazeta_for_iota_state
-	       (fst ts) env i (Cst_stack.add_cst term2 csts2) (EConstr.of_constr v2,sk2))
+	       (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
 	in
 	  ise_try evd [f3; f4]
 
     (* Eta-expansion *)
-    | Rigid, _ when EConstr.isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
-        eta env evd true sk1 (EConstr.Unsafe.to_constr term1) sk2 term2
+    | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
+        eta env evd true sk1 term1 sk2 term2
 
-    | _, Rigid when EConstr.isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 ->
-        eta env evd false sk2 (EConstr.Unsafe.to_constr term2) sk1 term1
+    | _, Rigid when isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 ->
+        eta env evd false sk2 term2 sk1 term1
 
     | Rigid, Rigid -> begin
-        let inj = EConstr.Unsafe.to_constr in
         match EConstr.kind evd term1, EConstr.kind evd term2 with
 
 	| Sort s1, Sort s2 when app_empty ->
@@ -794,11 +789,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
 	| Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty ->
             ise_and evd
-              [(fun i -> evar_conv_x ts env i CONV (inj c1) (inj c2));
+              [(fun i -> evar_conv_x ts env i CONV c1 c2);
                (fun i ->
- 	         let c = nf_evar i (inj c1) in
+ 	         let c = EConstr.to_constr i c1 in
                  let na = Nameops.name_max n1 n2 in
-	         evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty (inj c'1) (inj c'2))]
+	         evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
 
 	| Rel x1, Rel x2 ->
 	    if Int.equal x1 x2 then
@@ -842,11 +837,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             else UnifFailure (evd,NotSameHead)
 
 	| (Meta _, _) | (_, Meta _) ->
-          let inj = EConstr.Unsafe.to_constr in
 	  begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with
 	  |_, (UnifFailure _ as x) -> x
-	  |None, Success i' -> evar_conv_x ts env i' CONV (inj term1) (inj term2)
-	  |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (inj (Stack.zip i' (term1,sk1'))) (inj (Stack.zip i' (term2,sk2')))
+	  |None, Success i' -> evar_conv_x ts env i' CONV term1 term2
+	  |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2'))
 	  end
 
 	| (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ ->
@@ -884,38 +878,39 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 
      had to be initially resolved
   *)
+  let open EConstr in
   let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
   if Reductionops.Stack.compare_shape sk1 sk2 then
     let (evd',ks,_,test) =
       List.fold_left
 	(fun (i,ks,m,test) b ->
 	  if match n with Some n -> Int.equal m n | None -> false then
-	    let ty = Retyping.get_type_of env i (EConstr.of_constr t2) in
-	    let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in
+	    let ty = EConstr.of_constr (Retyping.get_type_of env i t2) in
+	    let test i = evar_conv_x trs env i CUMUL ty (Vars.substl ks b) in
 	      (i,t2::ks, m-1, test)
 	  else
 	    let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
 	    let i = Sigma.Unsafe.of_evar_map i in
-            let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
+            let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (EConstr.Unsafe.to_constr (Vars.substl ks b)) in
             let i' = Sigma.to_evar_map i' in
-	    (i', ev :: ks, m - 1,test))
+	    (i', EConstr.of_constr ev :: ks, m - 1,test))
 	(evd,[],List.length bs,fun i -> Success i) bs
     in
     let app = mkApp (c, Array.rev_of_list ks) in
     ise_and evd'
       [(fun i ->
 	exact_ise_stack2 env i
-          (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x))
+          (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (Vars.substl ks x))
           params1 params);
        (fun i ->
 	 exact_ise_stack2 env i
-           (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u))
+           (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (Vars.substl ks u))
            us2 us);
        (fun i -> evar_conv_x trs env i CONV c1 app);
        (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2);
        test;
        (fun i -> evar_conv_x trs env i CONV h2
-	 (fst (decompose_app_vect i (EConstr.of_constr (substl ks h)))))]
+	 (EConstr.of_constr (fst (decompose_app_vect i (Vars.substl ks h)))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
@@ -956,66 +951,69 @@ let set_evar_conv f = Hook.set evar_conv_hook_set f
 (* We assume here |l1| <= |l2| *)
 
 let first_order_unification ts env evd (ev1,l1) (term2,l2) =
+  let open EConstr in
   let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in
   ise_and evd
     (* First compare extra args for better failure message *)
-    [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) (Array.map EConstr.of_constr rest2) (Array.map EConstr.of_constr l1));
+    [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1);
     (fun i ->
       (* Then instantiate evar unless already done by unifying args *)
       let t2 = mkApp(term2,deb2) in
       if is_defined i (fst ev1) then
 	evar_conv_x ts env i CONV t2 (mkEvar ev1)
       else
-        let ev1 = (fst ev1, Array.map EConstr.of_constr (snd ev1)) in
-	solve_simple_eqn ~choose:true (to_conv_fun (evar_conv_x ts)) env i (None,ev1, EConstr.of_constr t2))]
+	solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find_undefined evd evk in
   let subst = make_pure_subst evi args in
-  let subst' = List.filter (fun (id,c) -> Term.eq_constr c term) subst in
+  let subst' = List.filter (fun (id,c) -> EConstr.eq_constr evd c term) subst in
   match subst' with
   | [] -> None
-  | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
+  | (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd)
 
 let apply_on_subterm env evdref f c t =
+  let open EConstr in
   let rec applyrec (env,(k,c) as acc) t =
     (* By using eq_constr, we make an approximation, for instance, we *)
     (* could also be interested in finding a term u convertible to t *)
     (* such that c occurs in u *)
-    if e_eq_constr_univs evdref c t then f k
+    if e_eq_constr_univs evdref (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t) then f k
     else
-      match kind_of_term t with
-      | Evar (evk,args) when Evd.is_undefined !evdref evk ->
+      match EConstr.kind !evdref t with
+      | Evar (evk,args) ->
           let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
           let g decl a = if is_local_assum decl then applyrec acc a else a in
           mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
       | _ ->
-        map_constr_with_binders_left_to_right
-	  (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
-	  applyrec acc t
+        let self acc c = EConstr.Unsafe.to_constr (applyrec acc (EConstr.of_constr c)) in
+        EConstr.of_constr (map_constr_with_binders_left_to_right
+	  (fun d (env,(k,c)) -> (push_rel d env, (k+1,Vars.lift 1 c)))
+	  self acc (EConstr.Unsafe.to_constr t))
   in
   applyrec (env,(0,c)) t
 
 let filter_possible_projections evd c ty ctxt args =
   (* Since args in the types will be replaced by holes, we count the
      fv of args to have a well-typed filter; don't know how necessary
-     it is however to have a well-typed filter here *)
-  let fv1 = free_rels evd (EConstr.of_constr (mkApp (c,args))) (* Hack: locally untyped *) in
-  let fv2 = collect_vars evd (EConstr.of_constr (mkApp (c,args))) in
+    it is however to have a well-typed filter here *)
+  let open EConstr in
+  let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in
+  let fv2 = collect_vars evd (mkApp (c,args)) in
   let len = Array.length args in
-  let tyvars = collect_vars evd (EConstr.of_constr ty) in
+  let tyvars = collect_vars evd ty in
   List.map_i (fun i decl ->
     let () = assert (i < len) in
     let a = Array.unsafe_get args i in
     (match decl with
      | NamedDecl.LocalAssum _ -> false
-     | NamedDecl.LocalDef (_,c,_) -> not (isRel c || isVar c)) ||
+     | NamedDecl.LocalDef (_,c,_) -> not (isRel evd (EConstr.of_constr c) || isVar evd (EConstr.of_constr c))) ||
     a == c ||
     (* Here we make an approximation, for instance, we could also be *)
     (* interested in finding a term u convertible to c such that a occurs *)
     (* in u *)
-    isRel a && Int.Set.mem (destRel a) fv1 ||
-    isVar a && Id.Set.mem (destVar a) fv2 ||
+    isRel evd a && Int.Set.mem (destRel evd a) fv1 ||
+    isVar evd a && Id.Set.mem (destVar evd a) fv2 ||
     Id.Set.mem (NamedDecl.get_id decl) tyvars)
     0 ctxt
 
@@ -1042,6 +1040,7 @@ let set_solve_evars f = solve_evars := f
 exception TypingFailed of evar_map
 
 let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
+  let open EConstr in
   try
   let evi = Evd.find_undefined evd evk in
   let env_evar = evar_filtered_env evi in
@@ -1050,7 +1049,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in
 
   let rec make_subst = function
-  | decl'::ctxt', c::l, occs::occsl when isVarId (NamedDecl.get_id decl') c ->
+  | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c ->
       begin match occs with
       | Some _ ->
         error "Cannot force abstraction on identity instance."
@@ -1059,9 +1058,9 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       end
   | decl'::ctxt', c::l, occs::occsl ->
       let id = NamedDecl.get_id decl' in
-      let t = NamedDecl.get_type decl' in
+      let t = EConstr.of_constr (NamedDecl.get_type decl') in
       let evs = ref [] in
-      let ty = Retyping.get_type_of env_rhs evd (EConstr.of_constr c) in
+      let ty = EConstr.of_constr (Retyping.get_type_of env_rhs evd c) in
       let filter' = filter_possible_projections evd c ty ctxt args in
       (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl)
   | _, _, [] -> []
@@ -1075,13 +1074,13 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         | Some _ -> error "Selection of specific occurrences not supported"
         | None ->
         let evty = set_holes evdref cty subst in
-        let instance = Filter.filter_list filter instance in
+        let instance = List.map EConstr.Unsafe.to_constr (Filter.filter_list filter instance) in
         let evd = Sigma.Unsafe.of_evar_map !evdref in
-        let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in
+        let Sigma (ev, evd, _) = new_evar_instance sign evd (EConstr.Unsafe.to_constr evty) ~filter instance in
         let evd = Sigma.to_evar_map evd in
         evdref := evd;
-        evsref := (fst (destEvar ev),evty)::!evsref;
-        ev in
+        evsref := (fst (destEvar !evdref (EConstr.of_constr ev)),evty)::!evsref;
+        EConstr.of_constr ev in
       set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst
   | [] -> rhs in
 
@@ -1108,11 +1107,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
               (* We force abstraction over this unconstrained occurrence *)
               (* and we use typing to propagate this instantiation *)
               (* This is an arbitrary choice *)
-              let evd = Evd.define evk (mkVar id) evd in
+              let evd = Evd.define evk (Constr.mkVar id) evd in
               match evar_conv_x ts env_evar evd CUMUL idty evty with
               | UnifFailure _ -> error "Cannot find an instance"
               | Success evd ->
-              match reconsider_conv_pbs (to_conv_fun (evar_conv_x ts)) evd with
+              match reconsider_conv_pbs (evar_conv_x ts) evd with
               | UnifFailure _ -> error "Cannot find an instance"
               | Success evd ->
               evd
@@ -1126,16 +1125,20 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       force_instantiation evd !evsref
   | [] ->
     let evd = 
-      try Evarsolve.check_evar_instance evd evk (EConstr.of_constr rhs)
-	    (to_conv_fun (evar_conv_x full_transparent_state))
+      try Evarsolve.check_evar_instance evd evk rhs
+	    (evar_conv_x full_transparent_state)
       with IllTypedInstance _ -> raise (TypingFailed evd)
     in
-      Evd.define evk rhs evd 
+      Evd.define evk (EConstr.Unsafe.to_constr rhs) evd 
   in
   abstract_free_holes evd subst, true
   with TypingFailed evd -> evd, false
 
+let to_pb (pb, env, t1, t2) =
+  (pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2)
+
 let second_order_matching_with_args ts env evd pbty ev l t =
+  let open EConstr in
 (*
   let evd,ev = evar_absorb_arguments env evd ev l in
   let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in
@@ -1144,18 +1147,19 @@ let second_order_matching_with_args ts env evd pbty ev l t =
   else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
   if b then Success evd else
  *)
-  let pb = (pbty,env,mkApp(mkEvar ev,l),t) in
+  let pb = to_pb (pbty,env,mkApp(mkEvar ev,l),t) in
   UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))
 
 let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
+  let open EConstr in
   let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
   let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in
-  let (term1,l1 as appr1) = try destApp t1 with DestKO -> (t1, [||]) in
-  let (term2,l2 as appr2) = try destApp t2 with DestKO -> (t2, [||]) in
+  let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in
+  let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
   let app_empty = Array.is_empty l1 && Array.is_empty l2 in
-  match kind_of_term term1, kind_of_term term2 with
+  match EConstr.kind evd term1, EConstr.kind evd term2 with
   | Evar (evk1,args1), (Rel _|Var _) when app_empty
-      && List.for_all (fun a -> Term.eq_constr a term2 || isEvar a)
+      && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a)
         (remove_instance_local_defs evd evk1 args1) ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
@@ -1163,9 +1167,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       | Some evd -> Success evd
       | None ->
          let reason = ProblemBeyondCapabilities in
-         UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
+         UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason)))
   | (Rel _|Var _), Evar (evk2,args2) when app_empty
-      && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a)
+      && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
         (remove_instance_local_defs evd evk2 args2) ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
@@ -1173,16 +1177,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       | Some evd -> Success evd
       | None ->
          let reason = ProblemBeyondCapabilities in
-         UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
+         UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason)))
   | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
-      let f env evd pbty x y = is_fconv ~reds:ts pbty env evd (EConstr.of_constr x) (EConstr.of_constr y) in
-      Success (solve_refl ~can_drop:true (to_conv_fun f) env evd
-                 (position_problem true pbty) evk1 (Array.map EConstr.of_constr args1) (Array.map EConstr.of_constr args2))
+      let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
+      Success (solve_refl ~can_drop:true f env evd
+                 (position_problem true pbty) evk1 args1 args2)
   | Evar ev1, Evar ev2 when app_empty ->
-      let ev1 = (fst ev1, Array.map EConstr.of_constr (snd ev1)) in
-      let ev2 = (fst ev2, Array.map EConstr.of_constr (snd ev2)) in
       Success (solve_evar_evar ~force:true
-        (evar_define (to_conv_fun (evar_conv_x ts)) ~choose:true) (to_conv_fun (evar_conv_x ts)) env evd
+        (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd
         (position_problem true pbty) ev1 ev2)
   | Evar ev1,_ when Array.length l1 <= Array.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
@@ -1244,9 +1246,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
       | a::l ->
           try
             let conv_algo = evar_conv_x ts in
-            let evd = check_evar_instance evd evk (EConstr.of_constr a) (to_conv_fun conv_algo) in
+            let evd = check_evar_instance evd evk (EConstr.of_constr a) conv_algo in
             let evd = Evd.define evk a evd in
-            match reconsider_conv_pbs (to_conv_fun conv_algo) evd with
+            match reconsider_conv_pbs conv_algo evd with
             | Success evd -> solve_unconstrained_evars_with_candidates ts evd
             | UnifFailure _ -> aux l
           with
@@ -1265,7 +1267,7 @@ let solve_unconstrained_impossible_cases env evd =
       let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in
       let ty = j_type j in
       let conv_algo = evar_conv_x full_transparent_state in
-      let evd' = check_evar_instance evd' evk (EConstr.of_constr ty) (to_conv_fun conv_algo) in
+      let evd' = check_evar_instance evd' evk (EConstr.of_constr ty) conv_algo in
 	Evd.define evk ty evd' 
     | _ -> evd') evd evd
 
@@ -1275,7 +1277,7 @@ let consider_remaining_unif_problems env
   let rec aux evd pbs progress stuck =
     match pbs with
     | (pbty,env,t1,t2 as pb) :: pbs ->
-        (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with
+        (match apply_conversion_problem_heuristic ts env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) with
 	| Success evd' ->
 	    let (evd', rest) = extract_all_conv_pbs evd' in
             begin match rest with
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 6f736e562..a0ff924ef 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open EConstr
 open Environ
 open Reductionops
 open Evd
@@ -45,16 +46,16 @@ val check_problems_are_solved : env -> evar_map -> unit
 val check_conv_record : env -> evar_map -> 
   state -> state ->
   Univ.universe_context_set * (constr * constr) 
-  * constr * constr list * (EConstr.t Stack.t * EConstr.t Stack.t) *
-    (EConstr.t Stack.t * EConstr.t Stack.t) *
-    (EConstr.t Stack.t * EConstr.t Stack.t) * constr *
+  * constr * constr list * (constr Stack.t * constr Stack.t) *
+    (constr Stack.t * constr Stack.t) *
+    (constr Stack.t * constr Stack.t) * constr *
     (int option * constr)
 
 (** Try to solve problems of the form ?x[args] = c by second-order
     matching, using typing to select occurrences *)
 
 val second_order_matching : transparent_state -> env -> evar_map ->
-  existential -> occurrences option list -> constr -> evar_map * bool
+  EConstr.existential -> occurrences option list -> constr -> evar_map * bool
 
 (** Declare function to enforce evars resolution by using typing constraints *)
 
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 8026ff3e4..f372dbf06 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -160,7 +160,7 @@ let define_evar_as_lambda env evd (evk,args) =
   evd, mkLambda (na, dom, evbody)
 
 let rec evar_absorb_arguments env evd (evk,args as ev) = function
-  | [] -> evd, (evk, Array.map EConstr.Unsafe.to_constr args)
+  | [] -> evd,ev
   | a::l ->
       let open EConstr in
       (* TODO: optimize and avoid introducing intermediate evars *)
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index f6d0efba6..f7bf4636b 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -27,7 +27,7 @@ val mk_valcon : EConstr.constr -> val_constraint
     [?y[vars1:=args1,vars:=args]] with
     [vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *)
 val evar_absorb_arguments : env -> evar_map -> EConstr.existential -> EConstr.constr list ->
-  evar_map * existential
+  evar_map * EConstr.existential
 
 val split_tycon :
   Loc.t -> env ->  evar_map -> type_constraint ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index fbba682fc..570f95324 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -626,7 +626,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
  	let fixi = match fixkind with
 	  | GFix (vn,i) -> i
 	  | GCoFix i -> i
-	in e_conv env.ExtraEnv.env evdref ftys.(fixi) t
+	in e_conv env.ExtraEnv.env evdref (EConstr.of_constr ftys.(fixi)) (EConstr.of_constr t)
       | None -> true
     in
       (* Note: bodies are not used by push_rec_types, so [||] is safe *)
@@ -732,7 +732,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      match candargs with
 	      | [] -> [], j_val hj
 	      | arg :: args -> 
-		if e_conv env.ExtraEnv.env evdref (j_val hj) arg then
+		if e_conv env.ExtraEnv.env evdref (EConstr.of_constr (j_val hj)) (EConstr.of_constr arg) then
 		  args, nf_evar !evdref (j_val hj)
 		else [], j_val hj
 	    in
@@ -1088,7 +1088,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
 	match valcon with
 	| None -> tj
 	| Some v ->
-	    if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj
+	    if e_cumul env.ExtraEnv.env evdref (EConstr.of_constr v) (EConstr.of_constr tj.utj_val) then tj
 	    else
 	      error_unexpected_type
                 ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8c03329e2..11f71ee02 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -165,7 +165,7 @@ let rec is_class_type evd c =
     match kind_of_term c with
     | Prod (_, _, t) -> is_class_type evd t
     | Evar (e, _) when Evd.is_defined evd e ->
-      is_class_type evd (Evarutil.whd_head_evar evd c)
+      is_class_type evd (EConstr.Unsafe.to_constr (Evarutil.whd_head_evar evd (EConstr.of_constr c)))
     | _ -> is_class_constr c
       
 let is_class_evar evd evi =
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 1dcb5f945..64264cf08 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -57,7 +57,7 @@ let e_judge_of_apply env evdref funj argjv =
   | hj::restjl ->
       match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
       | Prod (_,c1,c2) ->
-	 if Evarconv.e_cumul env evdref hj.uj_type (EConstr.Unsafe.to_constr c1) then
+	 if Evarconv.e_cumul env evdref (EConstr.of_constr hj.uj_type) c1 then
 	   apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
 	 else
 	   error_cant_apply_bad_type env (n, EConstr.Unsafe.to_constr c1, hj.uj_type) funj argjv
@@ -75,7 +75,7 @@ let e_check_branch_types env evdref (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
     error_number_branches env cj (Array.length explft);
   for i = 0 to Array.length explft - 1 do
-    if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then
+    if not (Evarconv.e_cumul env evdref (EConstr.of_constr lfj.(i).uj_type) (EConstr.of_constr explft.(i))) then
       error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
   done
 
@@ -91,7 +91,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
     let pt' = whd_all env !evdref (EConstr.of_constr pt) in
     match kind_of_term pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-        if not (Evarconv.e_cumul env evdref a1 a1') then error ();
+        if not (Evarconv.e_cumul env evdref (EConstr.of_constr a1) (EConstr.of_constr a1')) then error ();
         srec (push_rel (LocalAssum (na1,a1)) env) t ar'
     | Sort s, [] ->
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
@@ -131,8 +131,8 @@ let check_type_fixpoint loc env evdref lna lar vdefj =
   let lt = Array.length vdefj in
     if Int.equal (Array.length lar) lt then
       for i = 0 to lt-1 do
-        if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type
-		  (lift lt lar.(i))) then
+        if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type)
+		  (EConstr.of_constr (lift lt lar.(i)))) then
           Pretype_errors.error_ill_typed_rec_body ~loc env !evdref
             i lna vdefj lar
       done
@@ -150,7 +150,7 @@ let check_allowed_sort env sigma ind c p =
 
 let e_judge_of_cast env evdref cj k tj =
   let expected_type = tj.utj_val in
-  if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
+  if not (Evarconv.e_cumul env evdref (EConstr.of_constr cj.uj_type) (EConstr.of_constr expected_type)) then
     error_actual_type env cj expected_type;
   { uj_val = mkCast (cj.uj_val, k, expected_type);
     uj_type = expected_type }
@@ -282,7 +282,7 @@ and execute_array env evdref = Array.map (execute env evdref)
 let e_check env evdref c t =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-  if not (Evarconv.e_cumul env evdref j.uj_type t) then
+  if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) (EConstr.of_constr t)) then
     error_actual_type env j (nf_evar !evdref t)
 
 (* Type of a constr *)
@@ -328,4 +328,4 @@ let e_solve_evars env evdref c =
   (* side-effect on evdref *)
   nf_evar !evdref c
 
-let _ = Evarconv.set_solve_evars e_solve_evars
+let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref (EConstr.Unsafe.to_constr c)))
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b8c9a93db..ac2f14051 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -123,7 +123,7 @@ let abstract_list_all_with_dependencies env evd typ c l =
   let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
   let evd,b =
     Evarconv.second_order_matching empty_transparent_state
-      env evd ev' argoccs c in
+      env evd ev' argoccs (EConstr.of_constr c) in
   if b then
     let p = nf_evar evd ev in
       evd, p
@@ -607,7 +607,7 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN =
   match subst_defined_metas_evars (metasubst,[]) tyN with
   | None -> sigma
   | Some n ->
-    if is_ground_term sigma m && is_ground_term sigma n then
+    if is_ground_term sigma (EConstr.of_constr m) && is_ground_term sigma (EConstr.of_constr n) then
       let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in
 	if b then sigma
 	else error_cannot_unify env sigma (m,n)
@@ -659,8 +659,8 @@ let eta_constructor_app env f l1 term =
 
 let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
   let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn) curm curn =
-    let cM = Evarutil.whd_head_evar sigma curm
-    and cN = Evarutil.whd_head_evar sigma curn in
+    let cM = EConstr.Unsafe.to_constr (Evarutil.whd_head_evar sigma (EConstr.of_constr curm))
+    and cN = EConstr.Unsafe.to_constr (Evarutil.whd_head_evar sigma (EConstr.of_constr curn)) in
     let () = 
       if !debug_unification then
 	Feedback.msg_debug (Termops.print_constr_env curenv cM ++ str" ~= " ++ Termops.print_constr_env curenv cN)
@@ -964,7 +964,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	 let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in
 	    if b then Some (sigma, metasubst, evarsubst)
 	    else 
-	      if is_ground_term sigma m1 && is_ground_term sigma n1 then
+	      if is_ground_term sigma (EConstr.of_constr m1) && is_ground_term sigma (EConstr.of_constr n1) then
 		error_cannot_unify curenv sigma (cM,cN)
 	      else None
     in
@@ -1036,12 +1036,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	List.fold_left
 	  (fun (evd,ks,m) b ->
 	    if match n with Some n -> Int.equal m n | None -> false then
-                (evd,t2::ks, m-1)
+                (evd,EConstr.Unsafe.to_constr t2::ks, m-1)
             else
               let mv = new_meta () in
 	      let evd' = meta_declare mv (substl ks b) evd in
 	      (evd', mkMeta mv :: ks, m - 1))
-	  (sigma,[],List.length bs) bs
+	  (sigma,[],List.length bs) (List.map EConstr.Unsafe.to_constr bs)
       in
       try
       let opt' = {opt with with_types = false} in
@@ -1053,9 +1053,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 			   (fun s u1 u -> unirec_rec curenvnb pb opt' s (inj u1) (substl ks (inj u)))
 			   substn params1 params in
       let (substn,_,_) = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s (inj u1) (inj u2)) substn ts ts1 in
-      let app = mkApp (c, Array.rev_of_list ks) in
+      let app = mkApp (EConstr.Unsafe.to_constr c, Array.rev_of_list ks) in
       (* let substn = unirec_rec curenvnb pb b false substn t cN in *)
-	unirec_rec curenvnb pb opt' substn c1 app
+	unirec_rec curenvnb pb opt' substn (EConstr.Unsafe.to_constr c1) app
       with Invalid_argument "Reductionops.Stack.fold2" ->
 	error_cannot_unify (fst curenvnb) sigma (cM,cN)
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1271,11 +1271,8 @@ let order_metas metas =
 
 (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
 
-let to_conv_fun f = (); fun env sigma pb c1 c2 ->
-  f env sigma pb (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2)
-
 let solve_simple_evar_eqn ts env evd ev rhs =
-  match solve_simple_eqn (to_conv_fun (Evarconv.evar_conv_x ts)) env evd (None,ev,EConstr.of_constr rhs) with
+  match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,EConstr.of_constr rhs) with
   | UnifFailure (evd,reason) ->
       error_cannot_unify env evd ~reason (EConstr.Unsafe.to_constr (EConstr.mkEvar ev),rhs);
   | Success evd ->
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index d4b308bbe..af5fa921f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -32,7 +32,7 @@ let define_and_solve_constraints evk c env evd =
   match
     List.fold_left
       (fun p (pbty,env,t1,t2) -> match p with
-	| Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2
+	| Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2)
 	| UnifFailure _ as x -> x) (Success evd)
       pbs
   with
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c7f5efd5a..67e216745 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -232,7 +232,7 @@ 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 c then raise Exit;
+        if Evarutil.has_undefined_evars sigma (EConstr.of_constr 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/stm/stm.ml b/stm/stm.ml
index 23d68c4b8..6012e3d2d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1703,9 +1703,10 @@ end = struct (* {{{ *)
       Future.purify (fun () ->
        let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in
        let g = Evd.find sigma0 r_goal in
+       let is_ground c = Evarutil.is_ground_term sigma0 (EConstr.of_constr c) in
        if not (
-         Evarutil.is_ground_term sigma0 Evd.(evar_concl g) &&
-         List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
+         is_ground Evd.(evar_concl g) &&
+         List.for_all (Context.Named.Declaration.for_all is_ground)
                       Evd.(evar_context g))
        then
          CErrors.user_err ~hdr:"STM" (strbrk("the par: goal selector supports ground "^
@@ -1719,7 +1720,7 @@ end = struct (* {{{ *)
         | Evd.Evar_empty -> RespNoProgress
         | Evd.Evar_defined t ->
             let t = Evarutil.nf_evar sigma t in
-            if Evarutil.is_ground_term sigma t then
+            if Evarutil.is_ground_term sigma (EConstr.of_constr t) then
               RespBuiltSubProof (t, Evd.evar_universe_context sigma)
             else CErrors.user_err ~hdr:"STM" (str"The solution is not ground")
        end) ()
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6fb90e7af..a31e581e8 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -264,7 +264,7 @@ let unify_resolve_refine poly flags =
       let sigma' =
         let evdref = ref sigma' in
         if not (Evarconv.e_cumul env ~ts:flags.core_unify_flags.modulo_delta
-                                      evdref cl.cl_concl concl) then
+                                      evdref (EConstr.of_constr cl.cl_concl) (EConstr.of_constr concl)) then
           Type_errors.error_actual_type env
             {Environ.uj_val = term; Environ.uj_type = cl.cl_concl}
             concl;
@@ -1506,7 +1506,7 @@ let not_evar c =
   | _ -> Proofview.tclUNIT ()
 
 let is_ground c gl =
-  if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
+  if Evarutil.is_ground_term (project gl) (EConstr.of_constr c) then tclIDTAC gl
   else tclFAIL 0 (str"Not ground") gl
 
 let autoapply c i gl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e87746a28..17038e42d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -626,7 +626,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   let evd = 
     if unsafe then Some (Tacmach.New.project gl)
     else
-      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl))
+      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) (EConstr.of_constr t1) (EConstr.of_constr t2) (Tacmach.New.project gl))
       with Evarconv.UnableToUnify _ -> None
   in
   match evd with
@@ -1167,7 +1167,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       (* is the default value typable with the expected type *)
       let dflt_typ = unsafe_type_of env sigma dflt in
       try
-	let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
+	let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) (EConstr.of_constr p_i) !evdref in
 	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
 	dflt
       with Evarconv.UnableToUnify _ ->
@@ -1185,7 +1185,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       with
 	| Some w ->
             let w_type = unsafe_type_of env sigma w in
-            if Evarconv.e_cumul env evdref w_type a then
+            if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr a) then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1c10cdfea..c2163a274 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3731,7 +3731,7 @@ let specialize_eqs id gl =
   let ty = Tacmach.pf_get_hyp_typ gl id in
   let evars = ref (project gl) in
   let unif env evars c1 c2 =
-    compare_upto_variables c1 c2 && Evarconv.e_conv env evars c1 c2
+    compare_upto_variables c1 c2 && Evarconv.e_conv env evars (EConstr.of_constr c1) (EConstr.of_constr c2)
   in
   let rec aux in_eqs ctx acc ty =
     match kind_of_term ty with
@@ -4275,7 +4275,7 @@ let check_expected_type env sigma (elimc,bl) elimt =
   let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
   let sigma = solve_evar_clause env sigma true cl bl in
   let (_,u,_) = destProd cl.cl_concl in
-  fun t -> Evarconv.e_cumul env (ref sigma) t u
+  fun t -> Evarconv.e_cumul env (ref sigma) (EConstr.of_constr t) (EConstr.of_constr u)
 
 let check_enough_applied env sigma elim =
   let sigma = Sigma.to_evar_map sigma in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c39b4dc25..33b96bc37 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -458,7 +458,7 @@ 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 concl then raise Exit;
+          if Evarutil.has_undefined_evars sigma (EConstr.of_constr concl) then raise Exit;
           let c, _, ctx =
             Pfedit.build_by_tactic env (Evd.evar_universe_context sigma)
                                    concl (Tacticals.New.tclCOMPLETE tac)
@@ -1578,7 +1578,7 @@ let vernac_check_may_eval redexp glopt rc =
   let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
   let c = nf c in
   let j =
-    if Evarutil.has_undefined_evars sigma' c then
+    if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then
       Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c))
     else
       (* OK to call kernel which does not support evars *)