From 0074c7201e77ae27fa1bd79e05a084729266c55b Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Thu, 4 Jul 2019 19:49:28 -0700
Subject: Fix #10399: dependent evars line empty

This was broken by change 6608f64.
---
 engine/evarutil.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'engine/evarutil.ml')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index c946125d3f..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
-- 
cgit v1.2.3