From 217bd80b651d2d12b05f74cf21485eb0fea8e3e3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Sep 2017 21:51:59 +0200
Subject: Refine does not evar-normalizes the goal preemptively.

---
 src/tac2core.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 37f1c99b15..cd39cb6f27 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -734,7 +734,8 @@ end
 (** (unit -> constr) -> unit *)
 let () = define1 "refine" begin fun bt c ->
   let c = thaw bt c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
+    let gl = Proofview.Goal.assume gl in
     Refine.generic_refine ~typecheck:true c gl
   end >>= fun () -> return v_unit
 end
-- 
cgit v1.2.3