diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-05 18:25:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-05 18:26:01 +0200 |
| commit | 214b9ab7969fae71dcf553c399cb1674e463d0e3 (patch) | |
| tree | 54d110b3814b9706203399e80d3249ccc21b1edc /tactics | |
| parent | 05bf15c39334fa88083ab96b936d0d6f89f19d4e (diff) | |
Remove a redundant typing phase in the [refine] tactic.
The refined term is still typechecked twice (not counting Qed). But there seem to be a bug in the typechecker whereby it sometimes return terms which have universe inconsistencies. Until this is fixed, I'll leave the second typing phase which seems to catch these inconsistencies. To remove it, it suffices to change the [unsafe] flag to [true].
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 698f46559..b71e51314 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -373,7 +373,7 @@ let refine_tac {Glob_term.closure=closure;term=term} = Pretyping.ltac_idents = closure.Glob_term.idents; } in let update evd = Pretyping.understand_ltac flags evd env lvar tycon term in - Proofview.Refine.refine_casted (fun h -> Proofview.Refine.update h update) <*> + Proofview.Refine.refine ~unsafe:false (fun h -> Proofview.Refine.update h update) <*> Proofview.V82.tactic (reduce refine_red_flags refine_locs) end |