From 06fad70ea35ce988891dc80c3c8223fb7f1f64c0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Sep 2016 11:32:18 +0200
Subject: [PATCH] Use lazymatch in iClear to avoid backtracking on errors.
---
proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 754ba2e55..1fabcf66a 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -58,7 +58,7 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
Tactic Notation "iClear" constr(Hs) :=
let rec go Hs :=
- match Hs with
+ lazymatch Hs with
| [] => idtac
| "★" :: ?Hs => eapply tac_clear_spatial; [env_cbv; reflexivity|go Hs]
| ?H :: ?Hs =>
--
GitLab