Dualize the unsafe flag of refine into typecheck and make it mandatory.

2 files changed, 16 insertions, 17 deletions

diff --git a/proofs/refine.ml b/proofs/refine.ml
index eab053f3a3..796b4b8377 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -69,7 +69,7 @@ let add_side_effect env = function
 let add_side_effects env effects =
   List.fold_left (fun env eff -> add_side_effect env eff) env effects
 
-let generic_refine ?(unsafe = false) f gl =
+let generic_refine ~typecheck f gl =
   let gl = Proofview.Goal.assume gl in
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
@@ -91,9 +91,9 @@ let generic_refine ?(unsafe = false) f gl =
   let env = add_side_effects env sideff in
   (** Check that the introduced evars are well-typed *)
   let fold accu ev = typecheck_evar ev env accu in
-  let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in
+  let sigma = if typecheck then CList.fold_left fold sigma evs else sigma in
   (** Check that the refined term is typesafe *)
-  let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in
+  let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
   (** Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
@@ -132,16 +132,16 @@ let lift c =
   Proofview.tclUNIT c
   end
 
-let make_refine_enter ?unsafe f gl = generic_refine ?unsafe (lift f) gl
+let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl
 
-let refine_one ?(unsafe = false) f =
-  Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
+let refine_one ~typecheck f =
+  Proofview.Goal.enter_one (make_refine_enter ~typecheck f)
 
-let refine ?(unsafe = false) f =
+let refine ~typecheck f =
   let f evd =
     let (evd,c) = f evd in (evd,((), c))
   in
-  Proofview.Goal.enter (make_refine_enter ~unsafe f)
+  Proofview.Goal.enter (make_refine_enter ~typecheck f)
 
 (** Useful definitions *)
 
@@ -153,7 +153,7 @@ let with_type env evd c t =
   in
   evd , j'.Environ.uj_val
 
-let refine_casted ?unsafe f = Proofview.Goal.enter begin fun gl ->
+let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl ->
   let gl = Proofview.Goal.assume gl in
   let concl = Proofview.Goal.concl gl in
   let env = Proofview.Goal.env gl in
@@ -161,7 +161,7 @@ let refine_casted ?unsafe f = Proofview.Goal.enter begin fun gl ->
     let (h, c) = f h in
     with_type env h c concl
   in
-  refine ?unsafe f
+  refine ~typecheck f
 end
 
 (** {7 solve_constraints}
diff --git a/proofs/refine.mli b/proofs/refine.mli
index cede9d4581..c1c57ecb8e 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -21,19 +21,18 @@ val pr_constr :
 
 (** {7 Refinement primitives} *)
 
-val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
-(** In [refine ?unsafe t], [t] is a term with holes under some
+val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
+(** In [refine ~typecheck t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
     raised during the interpretation of [t] are caught and result in
-    tactic failures. If [unsafe] is [false] (which is the default) [t] is
-    type-checked beforehand. *)
+    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
 
-val refine_one : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic
+val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic
 (** A variant of [refine] which assumes exactly one goal under focus *)
 
-val generic_refine : ?unsafe:bool -> ('a * EConstr.t) tactic ->
+val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
   [ `NF ] Proofview.Goal.t -> 'a tactic
 (** The general version of refine. *)
 
@@ -44,7 +43,7 @@ val with_type : Environ.env -> Evd.evar_map ->
 (** [with_type env sigma c t] ensures that [c] is of type [t]
     inserting a coercion if needed. *)
 
-val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
+val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
 (** Like {!refine} except the refined term is coerced to the conclusion of the
     current goal. *)