From 6332f43dfee3efc890c5f8fdc1b5b54942c16307 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 9 May 2017 09:55:40 +0200
Subject: Explicit the unsafe flag of all calls to Refine.refine.

---
 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 8e6a0f6a72..3cd0a8de85 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 		if not (Option.is_empty term) then
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
-                      Refine.refine (fun evm -> (evm,EConstr.of_constr (Option.get term)));
+                      Refine.refine ~unsafe:true (fun evm -> (evm,EConstr.of_constr (Option.get term)));
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]
-- 
cgit v1.2.3


From 0fad09306982a88ff8d633d36abdc440dd542ab3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 13 Jun 2017 10:33:56 +0200
Subject: Dualize the unsafe flag of refine into typecheck and make it
 mandatory.

---
 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 3cd0a8de85..aba61146c7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 		if not (Option.is_empty term) then
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
-                      Refine.refine ~unsafe:true (fun evm -> (evm,EConstr.of_constr (Option.get term)));
+                      Refine.refine ~typecheck:false (fun evm -> (evm,EConstr.of_constr (Option.get term)));
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]
-- 
cgit v1.2.3