From 94768d5647b0559e24ee065ba70a64714878f0f6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 20 Feb 2016 19:40:24 +0100
Subject: [PATCH] fix transitivity change
---
prelude/lexico.v | 2 +-
prelude/list.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/prelude/lexico.v b/prelude/lexico.v
index 1b92f9825..43ecf2cdf 100644
--- a/prelude/lexico.v
+++ b/prelude/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/prelude/list.v b/prelude/list.v
index 8541aa18c..025e8c278 100644
--- a/prelude/list.v
+++ b/prelude/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).
--
GitLab