From a68ee60934a936632837731da4db79eb8d582e9c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Feb 2017 19:36:46 +0100
Subject: [PATCH] Turn some matches into lazymatches to improve error
propagation.
---
theories/proofmode/tactics.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 0d99ef960..5c7637c9c 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -676,7 +676,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
let rec find_pat found pats :=
lazymatch pats with
| [] =>
- match found with
+ lazymatch found with
| true => idtac
| false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
@@ -684,7 +684,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IClear ?H :: ?pats => iClear H; find_pat found pats
| IClearFrame ?H :: ?pats => iFrame H; find_pat found pats
| ?pat :: ?pats =>
- match found with
+ lazymatch found with
| false => go H pat; find_pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
--
GitLab