From 0eac7a8c3f946ffd599c3756bda32742102a8460 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Feb 2017 20:28:12 +0100
Subject: [PATCH] Add a missing iStartProof.
---
theories/proofmode/tactics.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 61762f93c..f329c4624 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -158,6 +158,7 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
|intros pat].
Tactic Notation "iPureIntro" :=
+ iStartProof;
eapply tac_pure_intro;
[let P := match goal with |- FromPure ?P _ => P end in
apply _ || fail "iPureIntro:" P "not pure"|].
--
GitLab