diff options
Diffstat (limited to 'src/array/FArray.v')
| -rw-r--r-- | src/array/FArray.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/array/FArray.v b/src/array/FArray.v index 69edf75..e9ab8dd 100644 --- a/src/array/FArray.v +++ b/src/array/FArray.v @@ -130,7 +130,7 @@ Module Raw. Qed. Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''. - Proof. unfold ltk; eauto. Qed. + Proof. unfold ltk; eauto with typeclass_ordtype. Qed. Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. Proof. unfold ltk, eqk. intros. apply lt_not_eq; auto with smtcoq_array. Qed. |