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

(limited to 'stm')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 2b32838964..74a3ee035c 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -41,7 +41,7 @@ let simple_goal sigma g gs =
   let open Evd in
   let open Evarutil in
   let evi = Evd.find sigma g in
-  Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) &&
+  Set.is_empty (evars_of_term evi.evar_concl) &&
   Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
   not (List.exists (Proofview.depends_on sigma g) gs)
 
-- 
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.

---
 stm/proofBlockDelimiter.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 74a3ee035c..04f10e7399 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -41,8 +41,8 @@ let simple_goal sigma g gs =
   let open Evd in
   let open Evarutil in
   let evi = Evd.find sigma g in
-  Set.is_empty (evars_of_term evi.evar_concl) &&
-  Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
+  Set.is_empty (evars_of_term sigma evi.evar_concl) &&
+  Set.is_empty (evars_of_filtered_evar_info sigma (nf_evar_info sigma evi)) &&
   not (List.exists (Proofview.depends_on sigma g) gs)
 
 let is_focused_goal_simple ~doc id =
-- 
cgit v1.2.3