diff options
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 |