Fix divergence of Ltac match in 8.4

mit-plv · Nov 3, 2016 · daff502 · daff502
1 parent 652ea56
commit daff502
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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