Verified Commit 89174aca authored by Tej Chajed's avatar Tej Chajed

Fix introducing forall with "%" intro pattern

Fixes #307.
parent d53af0f6
...@@ -77,6 +77,17 @@ ...@@ -77,6 +77,17 @@
--------------------------------------∗ --------------------------------------∗
Q Q
"test_iIntros_forall_pure"
: string
1 subgoal
PROP : sbi
Ψ : nat → PROP
a : nat
============================
--------------------------------------∗
Ψ a → Ψ a
The command has indeed failed with message: The command has indeed failed with message:
No applicable tactic. No applicable tactic.
The command has indeed failed with message: The command has indeed failed with message:
......
...@@ -119,6 +119,15 @@ Proof. iIntros "-#HQ". done. Qed. ...@@ -119,6 +119,15 @@ Proof. iIntros "-#HQ". done. Qed.
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ φ P φ ψ P. Lemma test_iIntros_pure (ψ φ : Prop) P : ψ φ P φ ψ P.
Proof. iIntros (??) "H". auto. Qed. Proof. iIntros (??) "H". auto. Qed.
Check "test_iIntros_forall_pure".
Lemma test_iIntros_forall_pure (Ψ: nat PROP) :
x : nat, Ψ x Ψ x.
Proof.
iIntros "%".
(* should be a trivial implication now *)
Show. auto.
Qed.
Lemma test_iIntros_pure_not : @{PROP} ¬False . Lemma test_iIntros_pure_not : @{PROP} ¬False .
Proof. by iIntros (?). Qed. Proof. by iIntros (?). Qed.
......
...@@ -1525,7 +1525,7 @@ Ltac iIntros_go pats startproof := ...@@ -1525,7 +1525,7 @@ Ltac iIntros_go pats startproof :=
| false => idtac | false => idtac
end end
(* Optimizations to avoid generating fresh names *) (* Optimizations to avoid generating fresh names *)
| IPure :: ?pats => iIntro (?); iIntros_go pats startproof | IPure IGallinaAnon :: ?pats => iIntro (?); iIntros_go pats startproof
| IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false | IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
| IDrop :: ?pats => iIntro _; iIntros_go pats startproof | IDrop :: ?pats => iIntro _; iIntros_go pats startproof
| IIdent ?H :: ?pats => iIntro H; iIntros_go pats startproof | IIdent ?H :: ?pats => iIntro H; iIntros_go pats startproof
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment