Fix #10399: dependent evars line empty

This was broken by change 6608f64.

4 files changed, 21 insertions, 8 deletions

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
diff --git a/engine/evd.ml b/engine/evd.ml
index 6a721a1a8a..099c83abf1 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1403,7 +1403,16 @@ end
 
 let evars_of_term evd c =
   let rec evrec acc c =
-    match MiniEConstr.kind evd c with
+    let c = MiniEConstr.whd_evar evd c in
+    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 evar_nodes_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
diff --git a/engine/evd.mli b/engine/evd.mli
index 132f7bc745..5ab53947f7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -509,6 +509,10 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
 val evars_of_term : evar_map -> econstr -> Evar.Set.t
   (** including evars in instances of evars *)
 
+val evar_nodes_of_term : econstr -> Evar.Set.t
+  (** same as evars_of_term but also including defined evars.
+      For use in printing dependent evars *)
+
 val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t
 
 val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 1f076470c1..d6f5aab1d1 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1247,7 +1247,7 @@ module V82 = struct
 
   let top_evars initial { solution=sigma; } =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term sigma c)
+      Evar.Set.elements (Evd.evar_nodes_of_term c)
     in
     CList.flatten (CList.map evars_of_initial initial)