Merge PR #8893: Moving evars_of_term from constr to econstr

Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: herbelin
Reviewed-by: maximedenes
Reviewed-by: ppedrot

16 files changed, 93 insertions, 94 deletions

diff --git a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh
new file mode 100644
index 0000000000..dc39ea5ef0
--- /dev/null
+++ b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh
@@ -0,0 +1,7 @@
+if [ "$CI_PULL_REQUEST" = "8893" ] || [ "$CI_BRANCH" = "master+moving-evars-of-term-on-econstr" ]; then
+
+    equations_CI_BRANCH=master+fix-evars_of_term-pr8893
+    equations_CI_REF=master+fix-evars_of_term-pr8893
+    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index be0318fbde..0a5bba39b9 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -656,26 +656,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids =
 (* spiwack: a few functions to gather evars on which goals depend. *)
 let queue_set q is_dependent set =
   Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
-let queue_term q is_dependent c =
-  queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c))
+let queue_term evm q is_dependent c =
+  queue_set q is_dependent (evars_of_term evm c)
 
 let process_dependent_evar q acc evm is_dependent e =
   let evi = Evd.find evm e in
   (* Queues evars appearing in the types of the goal (conclusion, then
      hypotheses), they are all dependent. *)
-  queue_term q true evi.evar_concl;
+  queue_term evm q true evi.evar_concl;
   List.iter begin fun decl ->
     let open NamedDecl in
-    queue_term q true (NamedDecl.get_type decl);
+    queue_term evm q true (NamedDecl.get_type decl);
     match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,b,_) -> queue_term q true b
+    | LocalDef (_,b,_) -> queue_term evm q true b
   end (EConstr.named_context_of_val evi.evar_hyps);
   match evi.evar_body with
   | Evar_empty ->
       if is_dependent then Evar.Map.add e None acc else acc
   | Evar_defined b ->
-      let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in
+      let subevars = evars_of_term evm b in
       (* evars appearing in the definition of an evar [e] are marked
          as dependent when [e] is dependent itself: if [e] is a
          non-dependent goal, then, unless they are reach from another
@@ -795,7 +795,7 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi =
   in
   let accu = match evi.evar_body with
   | Evar_empty -> Evar.Set.empty
-  | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b)
+  | Evar_defined b -> evars_of_term sigma b
   in
   let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in
   let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in
diff --git a/engine/evd.ml b/engine/evd.ml
index d37b49e2dc..0f10a380d3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -823,33 +823,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
   | Evar (evk2,_) -> fst (evar_source evk2 evd)
   | _             -> None
 
-(** The following functions return the set of evars immediately
-    contained in the object *)
-
-(* excluding defined evars *)
-
-let evars_of_term c =
-  let rec evrec acc c =
-    match kind c with
-    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
-    | _ -> Constr.fold evrec acc c
-  in
-  evrec Evar.Set.empty c
-
-let evars_of_named_context nc =
-  Context.Named.fold_outside
-    (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr)))
-    nc
-    ~init:Evar.Set.empty
-
-let evars_of_filtered_evar_info evi =
-  Evar.Set.union (evars_of_term evi.evar_concl)
-    (Evar.Set.union
-	(match evi.evar_body with
-	| Evar_empty -> Evar.Set.empty
-	| Evar_defined b -> evars_of_term b)
-	(evars_of_named_context (evar_filtered_context evi)))
-
 (**********************************************************)
 (* Sort variables *)
 
@@ -1404,3 +1377,30 @@ module MiniEConstr = struct
   let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
 
 end
+
+(** The following functions return the set of evars immediately
+    contained in the object *)
+
+(* excluding defined evars *)
+
+let evars_of_term evd c =
+  let rec evrec acc c =
+    match MiniEConstr.kind evd c with
+    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+    | _ -> Constr.fold evrec acc c
+  in
+  evrec Evar.Set.empty c
+
+let evars_of_named_context evd nc =
+  Context.Named.fold_outside
+    (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term evd constr)))
+    nc
+    ~init:Evar.Set.empty
+
+let evars_of_filtered_evar_info evd evi =
+  Evar.Set.union (evars_of_term evd evi.evar_concl)
+    (Evar.Set.union
+       (match evi.evar_body with
+       | Evar_empty -> Evar.Set.empty
+       | Evar_defined b -> evars_of_term evd b)
+       (evars_of_named_context evd (evar_filtered_context evi)))
diff --git a/engine/evd.mli b/engine/evd.mli
index 29235050b0..587a1de044 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -491,16 +491,15 @@ val extract_changed_conv_pbs : evar_map ->
 val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
 val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
 
-(** The following functions return the set of evars immediately
-    contained in the object; need the term to be evar-normal otherwise
-    defined evars are returned too. *)
+(** The following functions return the set of undefined evars
+    contained in the object. *)
 
-val evars_of_term : constr -> Evar.Set.t
+val evars_of_term : evar_map -> econstr -> Evar.Set.t
   (** including evars in instances of evars *)
 
-val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t
+val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t
 
-val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
+val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t
 
 (** Metas *)
 val meta_list : evar_map -> (metavariable * clbinding) list
diff --git a/engine/proofview.ml b/engine/proofview.ml
index ecea637947..1fd8b5d50e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -641,7 +641,7 @@ let shelve_goals l =
     [sigma]. *)
 let depends_on sigma src tgt =
   let evi = Evd.find sigma tgt in
-  Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
+  Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (Evarutil.nf_evar_info sigma evi))
 
 let unifiable_delayed g l =
   CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l
@@ -1251,9 +1251,9 @@ module V82 = struct
     let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }
 
-  let top_evars initial =
+  let top_evars initial { solution=sigma; } =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
+      Evar.Set.elements (Evd.evars_of_term sigma c)
     in
     CList.flatten (CList.map evars_of_initial initial)
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 92f8b86df5..b7ff3ac432 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -595,7 +595,7 @@ module V82 : sig
   val top_goals : entry -> proofview -> Evar.t list Evd.sigma
 
   (* returns the existential variable used to start the proof *)
-  val top_evars : entry -> Evar.t list
+  val top_evars : entry -> proofview -> Evar.t list
 
   (* Caution: this function loses quite a bit of information. It
      should be avoided as much as possible.  It should work as
diff --git a/engine/termops.ml b/engine/termops.ml
index 8a6bd17948..fcacb53ac4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -187,7 +187,7 @@ let compute_evar_dependency_graph sigma =
     in
     match evar_body evi with
     | Evar_empty -> acc
-    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc
+    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term sigma c) acc
   in
   Evd.fold fold sigma EvMap.empty
 
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 075ebf006a..0a5c85f4ab 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -290,7 +290,7 @@ let finalize_view s0 ?(simple_types=true) p =
 Goal.enter_one ~__LOC__ begin fun g ->
   let env = Goal.env g in
   let sigma = Goal.sigma g in
-  let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
+  let evars_of_p = Evd.evars_of_term sigma p in
   let filter x _ = Evar.Set.mem x evars_of_p in
   let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
   let p = Reductionops.nf_evar sigma p in
@@ -307,7 +307,7 @@ Goal.enter_one ~__LOC__ begin fun g ->
   let und0 = (* Unassigned evars in the initial goal *)
     let sigma0 = Tacmach.project s0 in
     let g0info = Evd.find sigma0 (Tacmach.sig_it s0) in
-    let g0 = Evd.evars_of_filtered_evar_info g0info in
+    let g0 = Evd.evars_of_filtered_evar_info sigma0 g0info in
     List.filter (fun k -> Evar.Set.mem k g0)
       (List.map fst (Evar.Map.bindings (Evd.undefined_map sigma0))) in
   let rigid = rigid_of und0 in
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 4e0866a0c5..adbcfb8f3b 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -529,8 +529,8 @@ exception FoundUnif of (evar_map * UState.t * tpattern)
 (* Note: we don't update env as we descend into the term, as the primitive *)
 (* unification procedure always rejects subterms with bound variables.     *)
 
-let dont_impact_evars_in cl =
-  let evs_in_cl = Evd.evars_of_term cl in
+let dont_impact_evars_in sigma0 cl =
+  let evs_in_cl = Evd.evars_of_term sigma0 cl in
   fun sigma -> Evar.Set.for_all (fun k ->
     try let _ = Evd.find_undefined sigma k in true
     with Not_found -> false) evs_in_cl
@@ -544,7 +544,7 @@ let dont_impact_evars_in cl =
 (*  - w_unify expands let-in (zeta conversion) eagerly, whereas we want to  *)
 (*    match a head let rigidly.                                             *)
 let match_upats_FO upats env sigma0 ise orig_c =
-  let dont_impact_evars = dont_impact_evars_in orig_c in
+  let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr orig_c) in
   let rec loop c =
     let f, a = splay_app ise c in let i0 = ref (-1) in
     let fpats =
@@ -586,7 +586,7 @@ let match_upats_FO upats env sigma0 ise orig_c =
 
 
 let match_upats_HO ~on_instance upats env sigma0 ise c =
- let dont_impact_evars = dont_impact_evars_in c in
+ let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr c) in
  let it_did_match = ref false in
  let failed_because_of_TC = ref false in
  let rec aux upats env sigma0 ise c =
diff --git a/proofs/proof.ml b/proofs/proof.ml
index ce7354aa62..09e4e898fe 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -425,7 +425,7 @@ module V82 = struct
     { Evd.it=List.hd gls ; sigma=sigma; }
 
   let top_evars p =
-    Proofview.V82.top_evars p.entry
+    Proofview.V82.top_evars p.entry p.proofview
 
   let grab_evars p =
     if not (is_done p) then
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 2b32838964..04f10e7399 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -41,8 +41,8 @@ let simple_goal sigma g gs =
   let open Evd in
   let open Evarutil in
   let evi = Evd.find sigma g in
-  Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) &&
-  Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
+  Set.is_empty (evars_of_term sigma evi.evar_concl) &&
+  Set.is_empty (evars_of_filtered_evar_info sigma (nf_evar_info sigma evi)) &&
   not (List.exists (Proofview.depends_on sigma g) gs)
 
 let is_focused_goal_simple ~doc id =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 9f233a2551..ece9fc8937 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -374,6 +374,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
     let obls, constr, typ =
       match term with
       | Some t ->
+        let termtype = EConstr.of_constr termtype in
         let obls, _, constr, typ =
           Obligations.eterm_obligations env id sigma 0 t termtype
         in obls, Some constr, typ
@@ -400,7 +401,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
           if not (Option.is_empty term) then
             let init_refine =
               Tacticals.New.tclTHENLIST [
-                Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
+                Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term));
                 Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
                 Tactics.New.reduce_after_refine;
               ]
@@ -497,10 +498,10 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program
   (* Check that the type is free of evars now. *)
   Pretyping.check_evars env (Evd.from_env env) sigma termtype;
   let termtype = to_constr sigma termtype in
-  let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
   let pstate =
     if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
-      (declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype;
+      let term = to_constr sigma (Option.get term) in
+      (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype;
        None)
     else if program_mode || refine || Option.is_empty props then
       declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 12df3215ad..d2c986fe5c 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -88,11 +88,12 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct
     let (c,ctx), sideff = Future.force ce.const_entry_body in
     assert(Safe_typing.empty_private_constants = sideff);
     assert(Univ.ContextSet.is_empty ctx);
+    Obligations.check_evars env evd;
+    let c = EConstr.of_constr c in
     let typ = match ce.const_entry_type with
-      | Some t -> t
-      | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+      | Some t -> EConstr.of_constr t
+      | None -> Retyping.get_type_of env evd c
     in
-    Obligations.check_evars env evd;
     let obls, _, c, cty =
       Obligations.eterm_obligations env ident evd 0 c typ
     in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 20a2db7ca2..69e2a209eb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -230,12 +230,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   in
   (* XXX: Capturing sigma here... bad bad *)
   let hook = Lemmas.mk_hook (hook sigma) in
-  (* XXX: Grounding non-ground terms here... bad bad *)
-  let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
-  let fullctyp = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   Obligations.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
-    Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp
+    Obligations.eterm_obligations env recname sigma 0 def typ
   in
   let ctx = Evd.evar_universe_context sigma in
     ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
@@ -246,7 +243,7 @@ let out_def = function
   | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.")
 
 let collect_evars_of_term evd c ty =
-  let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in
+  let evars = Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) in
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
@@ -262,17 +259,13 @@ let do_program_recursive local poly fixkind fixl ntns =
   let evd = nf_evar_map_undefined evd in
   let collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
-    let def =
-      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign)
-    and typ =
-      (* Worrying... *)
-      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
-    in
+    let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
+    let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
       Obligations.eterm_obligations env id evm
-        (List.length rec_sign) def typ
-    in (id, def, typ, imps, evars)
+        (List.length rec_sign) def typ in
+    (id, def, typ, imps, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1b1c618dc7..f768278dd7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -39,7 +39,7 @@ let check_evars env evm =
 
 type oblinfo =
   { ev_name: int * Id.t;
-    ev_hyps: Constr.named_context;
+    ev_hyps: EConstr.named_context;
     ev_status: bool * Evar_kinds.obligation_definition_status;
     ev_chop: int option;
     ev_src: Evar_kinds.t Loc.located;
@@ -50,11 +50,11 @@ type oblinfo =
 (** Substitute evar references in t using de Bruijn indices,
   where n binders were passed through. *)
 
-let subst_evar_constr evs n idf t =
+let subst_evar_constr evm evs n idf t =
   let seen = ref Int.Set.empty in
   let transparent = ref Id.Set.empty in
   let evar_info id = List.assoc_f Evar.equal id evs in
-  let rec substrec (depth, fixrels) c = match Constr.kind c with
+  let rec substrec (depth, fixrels) c = match EConstr.kind evm c with
     | Evar (k, args) ->
 	let { ev_name = (id, idstr) ;
 	      ev_hyps = hyps ; ev_chop = chop } =
@@ -84,18 +84,18 @@ let subst_evar_constr evs n idf t =
 	  in aux hyps args []
 	in
 	  if List.exists
-            (fun x -> match Constr.kind x with
+            (fun x -> match EConstr.kind evm x with
             | Rel n -> Int.List.mem n fixrels
             | _ -> false) args
           then
 	    transparent := Id.Set.add idstr !transparent;
-	  mkApp (idf idstr, Array.of_list args)
+          EConstr.mkApp (idf idstr, Array.of_list args)
     | Fix _ ->
-	Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c
-    | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c
+        EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c
+    | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c
   in
   let t' = substrec (0, []) t in
-    t', !seen, !transparent
+    EConstr.to_constr evm t', !seen, !transparent
 
 
 (** Substitute variable references in t using de Bruijn indices,
@@ -112,18 +112,18 @@ let subst_vars acc n t =
     to a product : forall H1 : t1, ..., forall Hn : tn, concl.
     Changes evars and hypothesis references to variable references.
 *)
-let etype_of_evar evs hyps concl =
+let etype_of_evar evm evs hyps concl =
   let open Context.Named.Declaration in
   let rec aux acc n = function
       decl :: tl ->
-	let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in
+        let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in
 	let t'' = subst_vars acc 0 t' in
 	let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
 	let s' = Int.Set.union s s' in
 	let trans' = Id.Set.union trans trans' in
 	  (match decl with
             | LocalDef (id,c,_) ->
-		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
+                let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
 		let c' = subst_vars acc 0 c' in
                   mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
 		Int.Set.union s'' s',
@@ -131,7 +131,7 @@ let etype_of_evar evs hyps concl =
             | LocalAssum (id,_) ->
                 mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
     | [] ->
-	let t', s, trans = subst_evar_constr evs n mkVar concl in
+        let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
 	  subst_vars acc 0 t', s, trans
   in aux [] 0 (List.rev hyps)
 
@@ -151,7 +151,7 @@ let evar_dependencies evm oev =
   let one_step deps =
     Evar.Set.fold (fun ev s ->
       let evi = Evd.find evm ev in
-      let deps' = evars_of_filtered_evar_info evi in
+      let deps' = evars_of_filtered_evar_info evm evi in
       if Evar.Set.mem oev deps' then
         invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev)
       else Evar.Set.union deps' s)
@@ -209,9 +209,7 @@ let eterm_obligations env name evm fs ?status t ty =
       (fun (id, (n, nstr), ev) l ->
 	 let hyps = Evd.evar_filtered_context ev in
          let hyps = trunc_named_context nc_len hyps in
-         let hyps = EConstr.Unsafe.to_named_context hyps in
-         let concl = EConstr.Unsafe.to_constr ev.evar_concl in
-         let evtyp, deps, transp = etype_of_evar l hyps concl in
+         let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in
 	 let evtyp, hyps, chop =
 	   match chop_product fs evtyp with
 	   | Some t -> t, trunc_named_context fs hyps, fs
@@ -237,9 +235,9 @@ let eterm_obligations env name evm fs ?status t ty =
       evn []
   in
   let t', _, transparent = (* Substitute evar refs in the term by variables *)
-    subst_evar_constr evts 0 mkVar t 
+    subst_evar_constr evm evts 0 EConstr.mkVar t
   in
-  let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
+  let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in
   let evars = 
     List.map (fun (ev, info) ->
       let { ev_name = (_, name); ev_status = force_status, status;
@@ -252,7 +250,7 @@ let eterm_obligations env name evm fs ?status t ty =
       in name, typ, src, (force_status, status), deps, tac) evts
   in
   let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
-  let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
+  let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in
     Array.of_list (List.rev evars), (evnames, evmap), t', ty
 
 let hide_obligation () =
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index d25daeed9c..9214ddd4b9 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -26,14 +26,14 @@ val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar
 (* env, id, evars, number of function prototypes to try to clear from
    evars contexts, object and type *)
 val eterm_obligations : env -> Id.t -> evar_map -> int ->
-  ?status:Evar_kinds.obligation_definition_status -> constr -> types ->
+  ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types ->
   (Id.t * types * Evar_kinds.t Loc.located *
      (bool * Evar_kinds.obligation_definition_status) * Int.Set.t *
       unit Proofview.tactic option) array
     (* Existential key, obl. name, type as product, 
        location of the original evar, associated tactic,
        status and dependencies as indexes into the array *)
-  * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
+  * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) *
     constr * types
     (* Translations from existential identifiers to obligation identifiers 
        and for terms with existentials to closed terms, given a