From daff502634feb935a0f24f24a5838a5863f1c2de Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 2 Nov 2016 20:04:06 -0400
Subject: Fix divergence of Ltac match in 8.4

---
 src/Util/PartiallyReifiedProp.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/Util/PartiallyReifiedProp.v')

diff --git a/src/Util/PartiallyReifiedProp.v b/src/Util/PartiallyReifiedProp.v
index b10d550ae..ef1567bd8 100644
--- a/src/Util/PartiallyReifiedProp.v
+++ b/src/Util/PartiallyReifiedProp.v
@@ -89,7 +89,9 @@ Definition reified_Prop_eq (x y : reified_Prop)
 Section rel.
   Local Ltac t :=
     cbv;
-    repeat (break_match
+    repeat (match goal with |- forall x, _ => intro end (* work around broken Ltac [match] in 8.4 that diverges on things under binders *)
+            || break_match
+            || break_match_hyps
             || intro
             || (simpl in * )
             || intuition try congruence
-- 
cgit v1.2.3