Verified Commit a14f0fa3 authored by Tej Chajed's avatar Tej Chajed

Add support for naming forall intros

parent 89174aca
......@@ -1097,6 +1097,7 @@ Ltac ltac_tactics.string_to_ident_hook ::=
make_string_to_ident_hook ltac:(fun s => lazymatch s with
| "HP2" => ident:(HP2)
| "H" => ident:(H)
| "y" => ident:(y)
| _ => fail 100 s
end).
......@@ -1111,6 +1112,10 @@ Proof.
exact (Himpl HP2).
Qed.
Lemma test_iIntros_forall_pure_named (Ψ: nat PROP) :
( x : nat, Ψ x) x : nat, Ψ x.
Proof. iIntros "HP". iIntros "%y". iApply ("HP" $! y). Qed.
Check "test_not_fresh".
Lemma test_not_fresh P1 (P2: Prop) (H:P2) :
P1 P2 - P1 P2.
......
......@@ -1525,6 +1525,8 @@ Ltac iIntros_go pats startproof :=
| false => idtac
end
(* Optimizations to avoid generating fresh names *)
| IPure (IGallinaNamed ?s) :: ?pats => let i := string_to_ident s in
iIntro (i); iIntros_go pats startproof
| IPure IGallinaAnon :: ?pats => iIntro (?); iIntros_go pats startproof
| IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
| IDrop :: ?pats => iIntro _; 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