From 3147b08a578aa42773eda8883161cd2018ceab8f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Jun 2019 13:55:53 +0200
Subject: [PATCH] Explicitly thunk tactic argument of `iPoseProofCoreLem`.
This avoids weird Ltac behaviors like those in !272.
Also, change `before_tc` keyword into `as` to be consistent with other tactics.
---
tests/proofmode.ref | 20 +++++++++-----------
theories/proofmode/ltac_tactics.v | 15 ++++++++-------
2 files changed, 17 insertions(+), 18 deletions(-)
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 4380630ab..9e44b1d37 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -554,17 +554,16 @@ Tactic failure: iStartProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)" and
+"iPoseProofCoreLem (constr) as (tactic3)" and
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
Tactic failure: iPoseProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)",
-"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
-"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
-"tac" (bound to fun H => iDestructHyp H as pat),
-"iDestructHyp (constr) as (constr)",
+"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
+fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
+fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
+fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iRename (constr) into (constr)", last call failed.
@@ -581,11 +580,10 @@ Tactic failure: iPoseProof: "Hx" not found.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)",
-"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
-"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
-"spec_tac" (bound to
-fun _ =>
+"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
+fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
+fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to
+fun Htmp =>
lazymatch lem with
| {| itrm := _; itrm_vars := ?xs; itrm_hyps := ?pat |} => iSpecializeCore
{| itrm := Htmp; itrm_vars := xs; itrm_hyps := pat |} as p
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index da4a2ec53..efd1bf784 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -725,8 +725,8 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
| _ => idtac
end.
-Tactic Notation "iPoseProofCoreLem"
- constr(lem) "as" constr(Hnew) "before_tc" tactic3(tac) :=
+Tactic Notation "iPoseProofCoreLem" constr(lem) "as" tactic3(tac) :=
+ let Hnew := iFresh in
eapply tac_pose_proof with Hnew _; (* (j:=H) *)
[iIntoEmpValid lem
|pm_reduce;
@@ -734,7 +734,7 @@ Tactic Notation "iPoseProofCoreLem"
| |- False =>
let Hnew := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
- | _ => tac
+ | _ => tac Hnew
end];
(* Solve all remaining TC premises generated by [iIntoEmpValid] *)
try iSolveTC.
@@ -1002,17 +1002,18 @@ whether the conclusion of the specialized term [lem] is persistent. *)
Tactic Notation "iPoseProofCore" open_constr(lem)
"as" constr(p) tactic3(tac) :=
iStartProof;
- let Htmp := iFresh in
let t := lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
- let spec_tac _ :=
+ let spec_tac Htmp :=
lazymatch lem with
| ITrm _ ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
| _ => idtac
end in
lazymatch type of t with
- | ident => iPoseProofCoreHyp t as Htmp; spec_tac (); [..|tac Htmp]
- | _ => iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
+ | ident =>
+ let Htmp := iFresh in
+ iPoseProofCoreHyp t as Htmp; spec_tac Htmp; [..|tac Htmp]
+ | _ => iPoseProofCoreLem t as (fun Htmp => spec_tac Htmp; [..|tac Htmp])
end.
(** * The apply tactic *)
--
GitLab