diff --git a/theories/lexico.v b/theories/lexico.v index 747bc83b3381031b8655589295c4f00558e37d65..42d6b31903ead119b0a1ebfc444a9c700707ab68 100644 --- a/theories/lexico.v +++ b/theories/lexico.v @@ -52,7 +52,7 @@ Proof. - intros [x y]. apply prod_lexico_irreflexive. by apply (irreflexivity lexico y). - intros [??] [??] [??] ??. - eapply prod_lexico_transitive; eauto. apply trans. + eapply prod_lexico_transitive; eauto. apply transitivity. Qed. Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)} `{Lexico B, tB : !TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _). diff --git a/theories/list.v b/theories/list.v index 9c536c242bf985c32c5370453d185eb7ee6ffa80..5042b8e842e602d33bede86426440c464f3b754b 100644 --- a/theories/list.v +++ b/theories/list.v @@ -2493,7 +2493,7 @@ Section Forall2_order. Global Instance: Symmetric R → Symmetric (Forall2 R). Proof. intros. induction 1; constructor; auto. Qed. Global Instance: Transitive R → Transitive (Forall2 R). - Proof. intros ????. apply Forall2_transitive. by apply @trans. Qed. + Proof. intros ????. apply Forall2_transitive. by apply @transitivity. Qed. Global Instance: Equivalence R → Equivalence (Forall2 R). Proof. split; apply _. Qed. Global Instance: PreOrder R → PreOrder (Forall2 R).