From f66b84de608830600e43f6d1a97c29226b6b58ea Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 4 Dec 2014 09:21:30 +0100 Subject: Refine primitive: [unsafe] is now true by default. Generally, tactics build type-correct terms. A safe refine is hence a waste of time (somtimes a significant one). The safe option is kept for specific purposes such as debugging, or some weird interaction with the pretyper and universes which still seemed to hold last time I checked (used by the user-level refine tactic). --- proofs/proofview.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 7f4ff6a5d..82dd9f6e7 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -961,7 +961,7 @@ struct let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"") () - let refine ?(unsafe = false) f = Goal.enter begin fun gl -> + let refine ?(unsafe = true) f = Goal.enter begin fun gl -> let sigma = Goal.sigma gl in let env = Goal.env gl in let concl = Goal.concl gl in @@ -1005,11 +1005,11 @@ struct in evd , j'.Environ.uj_val - let refine_casted ?(unsafe = false) f = Goal.enter begin fun gl -> + let refine_casted ?unsafe f = Goal.enter begin fun gl -> let concl = Goal.concl gl in let env = Goal.env gl in let f h = let (h, c) = f h in with_type env h c concl in - refine ~unsafe f + refine ?unsafe f end end -- cgit v1.2.3