From 214b9ab7969fae71dcf553c399cb1674e463d0e3 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 5 Sep 2014 18:25:27 +0200 Subject: 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]. --- tactics/extratactics.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') 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 -- cgit v1.2.3