diff options
| author | Matthieu Sozeau | 2016-10-21 10:49:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-21 12:24:43 +0200 |
| commit | 5b0b6c92354c34a4f0d5551f88b16264fb08be5f (patch) | |
| tree | b789f64d3024e70a70a1c175facab638dde76367 /ltac | |
| parent | a5b977e3acb6d2cd73ed6c895a7d4b587366caa9 (diff) | |
Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3
This makes [refine] typecheck the term only once (instead of twice),
(Qed excluded of course). Fix test-suite file for output of constraints
accordingly.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index db7318469f..d0318fb5f6 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -355,7 +355,7 @@ let refine_tac ist simple c = let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in - let refine = Refine.refine ~unsafe:false update in + let refine = Refine.refine ~unsafe:true update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> |