From 6211fd6e067e781a160db8765dd87067428048f2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 1 Nov 2018 23:26:06 +0100
Subject: Moving Evd.evars_of_term from constr to econstr + consequences.

This impacts a lot of code, apparently in the good, removing several
conversions back and forth constr.
---
 engine/evd.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 29235050b0..3cb4031f11 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -495,7 +495,7 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
     contained in the object; need the term to be evar-normal otherwise
     defined evars are returned too. *)
 
-val evars_of_term : constr -> Evar.Set.t
+val evars_of_term : econstr -> Evar.Set.t
   (** including evars in instances of evars *)
 
 val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t
-- 
cgit v1.2.3


From 6608f64f001f8f1a50b2dc41fefdf63c0b84b270 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 2 Nov 2018 00:17:47 +0100
Subject: Passing evar_map to evars_of_term rather than expecting the term to
 be evar-nf.

---
 engine/evd.mli | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 3cb4031f11..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 : econstr -> 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
-- 
cgit v1.2.3