Skip to content
Snippets Groups Projects
Commit 0eac7a8c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add a missing iStartProof.

parent ba714f5a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/tactics.v
+ 1
− 0
View file @ 0eac7a8c
...@@ -158,6 +158,7 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) := ...@@ -158,6 +158,7 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
|intros pat]. |intros pat].
Tactic Notation "iPureIntro" := Tactic Notation "iPureIntro" :=
iStartProof;
eapply tac_pure_intro; eapply tac_pure_intro;
[let P := match goal with |- FromPure ?P _ => P end in [let P := match goal with |- FromPure ?P _ => P end in
apply _ || fail "iPureIntro:" P "not pure"|]. apply _ || fail "iPureIntro:" P "not pure"|].
......
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