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.

---
 tactics/eqdecide.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/eqdecide.ml')

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 0cee4b6edb..10bc6e3e24 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -72,7 +72,7 @@ let generalize_right mk typ c1 c2 =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
-  Refine.refine ~unsafe:true begin fun sigma ->
+  Refine.refine ~typecheck:false begin fun sigma ->
     let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in
     let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
     let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
-- 
cgit v1.2.3