diff options
| author | Matthieu Sozeau | 2014-07-03 21:37:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-03 21:37:48 +0200 |
| commit | 84377c4d13418b0614d12a98a3f01421b52ac1e6 (patch) | |
| tree | 6887b2bed5976880e59289151da8285242da427f | |
| parent | e7ba2a9be24823503495e959f0dffc131e99801b (diff) | |
Restore proper order of effects in letin_tac_gen. Fixes CFGV again.
| -rw-r--r-- | tactics/tactics.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 078f2d0e0f..7420f9c102 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1774,15 +1774,16 @@ let letin_tac_gen with_eq abs ty = (Proofview.V82.tactic (thin_body [heq;id])) | None -> (Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in - Proofview.Goal.enter (fun gl -> - let (sigma,newcl,eq_tac) = eq_tac gl in - Tacticals.New.tclTHENLIST - [ Proofview.V82.tclEVARS sigma; - Proofview.V82.tclEVARUNIVCONTEXT ctx; - Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast); - intro_gen dloc (IntroMustBe id) (decode_hyp lastlhyp) true false; - Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls); - eq_tac ]) + Tacticals.New.tclTHEN + (Proofview.V82.tclEVARUNIVCONTEXT ctx) + (Proofview.Goal.enter (fun gl -> + let (sigma,newcl,eq_tac) = eq_tac gl in + Tacticals.New.tclTHENLIST + [ Proofview.V82.tclEVARS sigma; + Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast); + intro_gen dloc (IntroMustBe id) (decode_hyp lastlhyp) true false; + Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls); + eq_tac ])) end let letin_tac with_eq name c ty occs = |