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.

---
 API/API.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 20a637c1fa..5a833d08ad 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4100,7 +4100,7 @@ sig
 
   module New :
   sig
-    val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
+    val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
     val reduce_after_refine : unit Proofview.tactic
   end
   module Simple :
@@ -4490,7 +4490,7 @@ end
 
 module Refine :
 sig
-  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic
+  val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic
   val solve_constraints : unit Proofview.tactic
 end
 
-- 
cgit v1.2.3