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.
---
 plugins/ssr/ssrview.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 075ebf006a..57a068f82a 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -290,7 +290,7 @@ let finalize_view s0 ?(simple_types=true) p =
 Goal.enter_one ~__LOC__ begin fun g ->
   let env = Goal.env g in
   let sigma = Goal.sigma g in
-  let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
+  let evars_of_p = Evd.evars_of_term p in
   let filter x _ = Evar.Set.mem x evars_of_p in
   let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
   let p = Reductionops.nf_evar sigma p in
-- 
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.

---
 plugins/ssr/ssrview.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 57a068f82a..0a5c85f4ab 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -290,7 +290,7 @@ let finalize_view s0 ?(simple_types=true) p =
 Goal.enter_one ~__LOC__ begin fun g ->
   let env = Goal.env g in
   let sigma = Goal.sigma g in
-  let evars_of_p = Evd.evars_of_term p in
+  let evars_of_p = Evd.evars_of_term sigma p in
   let filter x _ = Evar.Set.mem x evars_of_p in
   let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
   let p = Reductionops.nf_evar sigma p in
@@ -307,7 +307,7 @@ Goal.enter_one ~__LOC__ begin fun g ->
   let und0 = (* Unassigned evars in the initial goal *)
     let sigma0 = Tacmach.project s0 in
     let g0info = Evd.find sigma0 (Tacmach.sig_it s0) in
-    let g0 = Evd.evars_of_filtered_evar_info g0info in
+    let g0 = Evd.evars_of_filtered_evar_info sigma0 g0info in
     List.filter (fun k -> Evar.Set.mem k g0)
       (List.map fst (Evar.Map.bindings (Evd.undefined_map sigma0))) in
   let rigid = rigid_of und0 in
-- 
cgit v1.2.3