diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-07-11 09:57:38 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-07-11 09:57:38 -0400 |
| commit | d8b643de8922f788328bbe356506a39b1f664ca6 (patch) | |
| tree | f01bba64db0090ee749a0ee6ae72399c3e1d3a6f /src | |
| parent | 8122a40b0cc60826b38460ef4a244b42a0999f48 (diff) | |
[congruence] is more powerful in 8.5 than in 8.4
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/Tuple.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 0d8d5975f..67827c4a6 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -154,7 +154,9 @@ end. Lemma from_list_default'_eq : forall {T} (d : T) xs n y pf, from_list_default' d y n xs = from_list' y n xs pf. Proof. - induction xs; destruct n; intros; simpl in *; congruence. + induction xs; destruct n; intros; simpl in *; + solve [ congruence (* 8.5 *) + | erewrite IHxs; reflexivity ]. (* 8.4 *) Qed. Lemma from_list_default_eq : forall {T} (d : T) xs n pf, |