diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-12-04 09:21:30 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-12-04 14:38:05 +0100 |
| commit | f66b84de608830600e43f6d1a97c29226b6b58ea (patch) | |
| tree | e8a4ecad63a04ee1462487aeafa58b301335b713 | |
| parent | 446b9c571c29f740475e39c19c4037b8102f1f21 (diff) | |
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).
| -rw-r--r-- | proofs/proofview.ml | 6 |
1 files 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"<constr>") () - 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 |