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/evd.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'engine/evd.mli')

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
-- 
cgit v1.2.3