From a1be30d3d426d7eeeacdb4500b222aa01790378e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 27 Oct 2016 11:29:15 +0200
Subject: [PATCH] Fix inefficiency in proof mode.
Since env_cbv does not unfold these apps, we should do it ourselves,
to avoid ending up with partially evaluated terms.
---
proofmode/tactics.v | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index d4d5431ad..2a4e168ef 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -308,7 +308,8 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
|(*goal*)
|go H1 pats]
| SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs) :: ?pats =>
- eapply tac_specialize_assert with _ _ _ H1 _ lr (Hs_frame ++ Hs) _ _ _ _;
+ let Hs' := eval cbv in (Hs_frame ++ Hs) in
+ eapply tac_specialize_assert with _ _ _ H1 _ lr Hs' _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|match m with
@@ -1084,7 +1085,8 @@ Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac)
|apply _ || fail "iAssert:" Q "not persistent"
|tac H]
| [SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs)] =>
- eapply tac_assert with _ _ _ lr (Hs_frame ++ Hs) H Q _;
+ let Hs' := eval compute in (Hs_frame ++ Hs) in
+ eapply tac_assert with _ _ _ lr Hs' H Q _;
[match m with
| false => apply elim_modal_dummy
| true => apply _ || fail "iAssert: goal not a modality"
--
GitLab