diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-05-09 10:03:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-06-13 10:32:32 +0200 |
| commit | 22ca6b0d70bb8b49aaa420f844c75592e5781c21 (patch) | |
| tree | 865c0332b3a52a1af6ae9ebc26a2e5eb07518de6 /proofs | |
| parent | 6332f43dfee3efc890c5f8fdc1b5b54942c16307 (diff) | |
Turn the default behaviour of the refine primitive into the safe one.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refine.ml | 6 | ||||
| -rw-r--r-- | proofs/refine.mli | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index caa6b9fb3..eab053f3a 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 = true) f gl = +let generic_refine ?(unsafe = false) f gl = let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -134,10 +134,10 @@ let lift c = let make_refine_enter ?unsafe f gl = generic_refine ?unsafe (lift f) gl -let refine_one ?(unsafe = true) f = +let refine_one ?(unsafe = false) f = Proofview.Goal.enter_one (make_refine_enter ~unsafe f) -let refine ?(unsafe = true) f = +let refine ?(unsafe = false) f = let f evd = let (evd,c) = f evd in (evd,((), c)) in diff --git a/proofs/refine.mli b/proofs/refine.mli index f1439f9a1..cede9d458 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -27,7 +27,7 @@ val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit 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] (default is [true]) [t] is + tactic failures. If [unsafe] is [false] (which is the default) [t] is type-checked beforehand. *) val refine_one : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic |