1 files changed, 15 insertions, 15 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index ea71be8e43..5444d88e47 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -661,26 +661,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 evm q is_dependent c =
-  queue_set q is_dependent (evars_of_term evm c)
+let queue_term q is_dependent c =
+  queue_set q is_dependent (evar_nodes_of_term 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 evm q true evi.evar_concl;
+  queue_term q true evi.evar_concl;
   List.iter begin fun decl ->
     let open NamedDecl in
-    queue_term evm q true (NamedDecl.get_type decl);
+    queue_term q true (NamedDecl.get_type decl);
     match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,b,_) -> queue_term evm q true b
+    | LocalDef (_,b,_) -> queue_term 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 evm b in
+      let subevars = evar_nodes_of_term 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
@@ -861,12 +861,12 @@ let compare_constructor_instances evd u u' =
   in
   Evd.add_universe_constraints evd soft
 
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
-    [u] up to existential variable instantiation and equalisable
-    universes. The term [t] is interpreted in [sigma1] while [u] is
-    interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extension of those in [sigma1]. *)
-let eq_constr_univs_test sigma1 sigma2 t u =
+(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
+    [t] and [u] up to existential variable instantiation and
+    equalisable universes. The term [t] is interpreted in [evd] while
+    [u] is interpreted in [extended_evd]. The universe constraints in
+    [extended_evd] are assumed to be an extension of those in [evd]. *)
+let eq_constr_univs_test ~evd ~extended_evd t u =
   (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
   let open Evd in
   let t = EConstr.Unsafe.to_constr t
@@ -877,8 +877,8 @@ let eq_constr_univs_test sigma1 sigma2 t u =
   in
   let ans =
     UnivProblem.eq_constr_univs_infer_with
-      (fun t -> kind_of_term_upto sigma1 t)
-      (fun u -> kind_of_term_upto sigma2 u)
-      (universes sigma2) fold t u sigma2
+      (fun t -> kind_of_term_upto evd t)
+      (fun u -> kind_of_term_upto extended_evd u)
+      (universes extended_evd) fold t u extended_evd
   in
   match ans with None -> false | Some _ -> true