diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-02 20:04:06 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-02 20:04:06 -0400 |
| commit | daff502634feb935a0f24f24a5838a5863f1c2de (patch) | |
| tree | 83e205b8b252b7acc02f254842640999959e5196 /src/Util/PartiallyReifiedProp.v | |
| parent | 652ea56a96637d0567d2f673c5ffd71600d04c67 (diff) | |
Fix divergence of Ltac match in 8.4
Diffstat (limited to 'src/Util/PartiallyReifiedProp.v')
| -rw-r--r-- | src/Util/PartiallyReifiedProp.v | 4 |
1 files changed, 3 insertions, 1 deletions
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 |