From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 31 Mar 2018 17:43:18 +0200
Subject: Evar maps contain econstrs.

We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
---
 stm/proofBlockDelimiter.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm/proofBlockDelimiter.ml')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 23f976120a..0af766219c 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 evi.evar_concl) &&
+  Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr 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