diff --git a/Makefile.coq.local b/Makefile.coq.local
index 8d426e9e706ade94428ead1e7dccc3396425aca7..4ebd9b87223b92f92001456e9b25c865c1ba8cdd 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -8,7 +8,8 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_BROKEN=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(9|10)\b" > /dev/null && echo 1)
+# In Coq 8.9, printing notations involving primitive notations is broken
+COQ_BROKEN=$(shell echo "$(COQ_VERSION)" | egrep "^8\.9\b" > /dev/null && echo 1)
# Can't use pipes because that discards error codes and dash provides no way to control that.
# Also egrep errors if it doesn't match anything, we have to ignore that.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 61197930c830bbb5941f78dea7fd448dd8ede82d..a3d7a44daa111266a551e9491dae681c28eceef3 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -454,14 +454,19 @@ Tactic failure: iStartProof: not a BI assertion.
"iPoseProof_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iPoseProof (open_constr) as (constr)" and
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", last call
-failed.
+In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
+"<iris.proofmode.ltac_tactics.iPoseProofCore_go>" 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)" and
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", last call
-failed.
+In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
+"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.
Tactic failure: iRename: "H" not fresh.
"iRevert_fail"
: string
@@ -474,15 +479,23 @@ Tactic failure: iElaborateSelPat: "H" not found.
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
-"iDestructCore (open_constr) as (constr) (tactic)" and
-"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
+"iDestructCore (open_constr) as (constr) (tactic)",
+"iDestructCore (open_constr) as (constr) (tactic)",
+"tac" (bound to fun H => iDestructHyp H as pat),
+"iDestructHyp (constr) as (constr)",
+"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
+"<iris.proofmode.ltac_tactics.iDestructHypFindPat>", last call failed.
Tactic failure: iDestruct: "{HP}"
should contain exactly one proper introduction pattern.
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
-"iDestructCore (open_constr) as (constr) (tactic)" and
-"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
+"iDestructCore (open_constr) as (constr) (tactic)",
+"iDestructCore (open_constr) as (constr) (tactic)",
+"tac" (bound to fun H => iDestructHyp H as pat),
+"iDestructHyp (constr) as (constr)",
+"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
+"<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
"iApply_fail"
@@ -493,8 +506,7 @@ In nested Ltac calls to "iApply (open_constr)",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
"<iris.proofmode.ltac_tactics.iPoseProofCore_go>",
-"goal_tac" (bound to
-fun _ => <ssreflect_plugin::ssrtclseq@0> spec_tac ltac:(()) ; last tac Htmp) and
-"<ssreflect_plugin::ssrtclseq@0> spec_tac ltac:(()) ; last tac Htmp", last
-call failed.
+"goal_tac" (bound to fun _ => spec_tac ltac:(()); [ .. | tac Htmp ]),
+"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
+failed.
Tactic failure: iApply: cannot apply P.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index f2fe3bd8e51d6798425ae34d1357eedad94011de..fda29fc12a90fc96d017e5eb99d1fab7343c74f1 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -107,6 +107,8 @@
--------------------------------------∗
|={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
+"test_iInv_12"
+ : string
The command has indeed failed with message:
In nested Ltac calls to "iInv (constr) as (constr)",
"iInvCore (constr) in (tactic)" and
@@ -125,6 +127,8 @@ In nested Ltac calls to "iInv (constr) as (constr)",
"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
failed.
Tactic failure: iInv: invariant "H2" not found.
+"test_iInv"
+ : string
1 subgoal
Σ : gFunctors
@@ -139,6 +143,8 @@ Tactic failure: iInv: invariant "H2" not found.
--------------------------------------∗
|={E ∖ ↑N}=> ⎡ ▷ 𓟠⎤ ∗ (|={E}=> emp)
+"test_iInv_with_close"
+ : string
1 subgoal
Σ : gFunctors
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 1cfc957441c25bf90b0c8eff4b390026ae44b5ee..0beb0b2d3aa6c036f0bc46f0d00c236cdeb87f77 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -202,6 +202,7 @@ Section iris_tests.
Qed.
(* error messages *)
+ Check "test_iInv_12".
Lemma test_iInv_12 N P: inv N (<pers> P) ={⊤}=∗ True.
Proof.
iIntros "H".
@@ -229,6 +230,7 @@ Section monpred_tests.
Implicit Types P Q R : monPred.
Implicit Types ð“Ÿ ð“ ð“¡ : iProp Σ.
+ Check "test_iInv".
Lemma test_iInv N E ð“Ÿ :
↑N ⊆ E →
⎡inv N ð“ŸâŽ¤ ⊢@{monPredI} |={E}=> emp.
@@ -238,6 +240,7 @@ Section monpred_tests.
iFrame "HP". auto.
Qed.
+ Check "test_iInv_with_close".
Lemma test_iInv_with_close N E ð“Ÿ :
↑N ⊆ E →
⎡inv N ð“ŸâŽ¤ ⊢@{monPredI} |={E}=> emp.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 93904be662d5b20cf0c60bb68eca8b126c51a7b7..94359d4b5a9f0fbcbba1362c5cf93f416d9efe2f 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -730,8 +730,19 @@ The tactic instantiates each dependent argument [x_i] with an evar and generates
a goal [R] for each non-dependent argument [x_i : R]. For example, if the
original goal was [Q] and [t] has type [∀ x, P x → Q], then it generates an evar
[?x] for [x] and a subgoal [P ?x]. *)
-Tactic Notation "iIntoEmpValid" open_constr(t) :=
- let rec go t :=
+Local Ltac iIntoEmpValid t :=
+ let go_specialize t tT :=
+ lazymatch tT with (* We do not use hnf of tT, because, if
+ entailment is not opaque, then it would
+ unfold it. *)
+ | ?P → ?Q => let H := fresh in assert P as H; [|iIntoEmpValid uconstr:(t H); clear H]
+ | ∀ _ : ?T, _ =>
+ (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
+ (* This is a workarround for Coq bug #6583. *)
+ let e := fresh in evar (e:id T);
+ let e' := eval unfold e in e in clear e; iIntoEmpValid (t e')
+ end
+ in
(* We try two reduction tactics for the type of t before trying to
specialize it. We first try the head normal form in order to
unfold all the definition that could hide an entailment. Then,
@@ -747,20 +758,7 @@ Tactic Notation "iIntoEmpValid" open_constr(t) :=
| let tT' := eval cbv zeta in tT in
notypeclasses refine (as_emp_valid_1 tT _ _);
[iSolveTC || fail 1 "iPoseProof: not a BI assertion"
- |exact t]]
- with go_specialize t tT :=
- lazymatch tT with (* We do not use hnf of tT, because, if
- entailment is not opaque, then it would
- unfold it. *)
- | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
- | ∀ _ : ?T, _ =>
- (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
- (* This is a workarround for Coq bug #6583. *)
- let e := fresh in evar (e:id T);
- let e' := eval unfold e in e in clear e; go (t e')
- end
- in
- go t.
+ |exact t]].
(* The tactic [tac] is called with a temporary fresh name [H]. The argument
[lazy_tc] denotes whether type class inference on the premises of [lem] should
@@ -802,8 +800,8 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
| _ => idtac
end in
lazymatch eval compute in lazy_tc with
- | true => iPoseProofCore_go Htmp t ltac:(fun _ => spec_tac (); last (tac Htmp))
- | false => iPoseProofCore_go Htmp t spec_tac; last (tac Htmp)
+ | true => iPoseProofCore_go Htmp t ltac:(fun _ => spec_tac (); [..| tac Htmp ])
+ | false => iPoseProofCore_go Htmp t spec_tac; [..| tac Htmp ]
end.
(** * Apply *)
@@ -1081,8 +1079,7 @@ Tactic Notation "iModCore" constr(H) :=
|pm_reflexivity|].
(** * Basic destruct tactic *)
-Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
- let rec go Hz pat :=
+Local Ltac iDestructHypGo Hz pat :=
lazymatch pat with
| IAnom =>
lazymatch Hz with
@@ -1093,36 +1090,37 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IFrame => iFrameHyp Hz
| IIdent ?y => iRename Hz into y
| IList [[]] => iExFalso; iExact Hz
- | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; go Hz pat1
- | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; go Hz pat2
+ | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat1
+ | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat2
| IList [[?pat1; ?pat2]] =>
- let Hy := iFresh in iAndDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
- | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
+ let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat1; iDestructHypGo Hy pat2
+ | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz pat2]
| IPureElim => iPure Hz as ?
| IRewrite Right => iPure Hz as ->
| IRewrite Left => iPure Hz as <-
- | IAlwaysElim ?pat => iPersistent Hz; go Hz pat
- | IModalElim ?pat => iModCore Hz; go Hz pat
+ | IAlwaysElim ?pat => iPersistent Hz; iDestructHypGo Hz pat
+ | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
| _ => fail "iDestruct:" pat "invalid"
- end in
- let rec find_pat found pats :=
+ end.
+Local Ltac iDestructHypFindPat H pat found pats :=
lazymatch pats with
| [] =>
lazymatch found with
| true => pm_prettify (* post-tactic prettification *)
| false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
- | ISimpl :: ?pats => simpl; find_pat found pats
- | IClear ?H :: ?pats => iClear H; find_pat found pats
- | IClearFrame ?H :: ?pats => iFrame H; find_pat found pats
+ | ISimpl :: ?pats => simpl; iDestructHypFindPat H pat found pats
+ | IClear ?H :: ?pats => iClear H; iDestructHypFindPat H pat found pats
+ | IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat H pat found pats
| ?pat :: ?pats =>
lazymatch found with
- | false => go H pat; find_pat true pats
+ | false => iDestructHypGo H pat; iDestructHypFindPat H pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
- end in
+ end.
+Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
let pats := intro_pat.parse pat in
- find_pat false pats.
+ iDestructHypFindPat H pat false pats.
Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
@@ -1537,10 +1535,10 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
(* persistent hypothesis, check for a CopyDestruct instance *)
tryif (let dummy := constr:(_ : CopyDestruct P) in idtac)
then (iPoseProofCore lem as p false tac)
- else (iSpecializeCore lem as p; last (tac H))
+ else (iSpecializeCore lem as p; [..| tac H])
| Some (false, ?P) =>
(* spatial hypothesis, cannot copy *)
- iSpecializeCore lem as p; last (tac H)
+ iSpecializeCore lem as p; [..| tac H ]
end
end
end.
@@ -2088,13 +2086,13 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
lazymatch type of select with
| string =>
eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat);
- first by (iAssumptionCore || fail "iInv: invariant" select "not found")
+ [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
| ident =>
eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat);
- first by (iAssumptionCore || fail "iInv: invariant" select "not found")
+ [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
| namespace =>
eapply @tac_inv_elim with (j:=H) (Pclose:=Pclose_pat);
- first by (iAssumptionInv select || fail "iInv: invariant" select "not found")
+ [ (by iAssumptionInv select) || fail "iInv: invariant" select "not found" |..]
| _ => fail "iInv: selector" select "is not of the right type "
end;
[iSolveTC ||