From 1805a4354dcc1c1b545914d0e92eea8a2ab619c1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 Jan 2017 13:29:02 +0100
Subject: [PATCH] Fix error messages of iAndDestructChoice.
---
theories/proofmode/tactics.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index d56432016..37d5655fd 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -565,10 +565,10 @@ Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(lr) constr(H') :=
eapply tac_and_destruct_choice with _ H _ lr H' _ _ _;
- [env_cbv; reflexivity || fail "iAndDestruct:" H "not found"
+ [env_cbv; reflexivity || fail "iAndDestructChoice:" H "not found"
|let P := match goal with |- IntoAnd _ ?P _ _ => P end in
- apply _ || fail "iAndDestruct: cannot destruct" P
- |env_cbv; reflexivity || fail "iAndDestruct:" H' " not fresh"|].
+ apply _ || fail "iAndDestructChoice: cannot destruct" P
+ |env_cbv; reflexivity || fail "iAndDestructChoice:" H' " not fresh"|].
Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
eapply tac_combine with _ _ _ H1 _ _ H2 _ _ H _;
--
GitLab