From 041ee4822cb247e60df51fa147175f8b16711df1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 22 Jan 2018 17:35:02 +0100
Subject: proofview: goals come with a state

---
 vernac/classes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 4a2dba859..241f07f2f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -334,7 +334,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
                       Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
-                      Proofview.Unsafe.tclNEWGOALS gls;
+                      Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
                       Tactics.New.reduce_after_refine;
                     ]
                   in
-- 
cgit v1.2.3