From d68bef532d2c8ba6ff1edc80815f9ba9cd3f2d8c Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Wed, 17 Nov 2021 23:31:28 +0100 Subject: [PATCH] drop unused compat lemma --- core/ordtype.v | 6 ------ core/pred.v | 2 +- 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/core/ordtype.v b/core/ordtype.v index 4ec1cad..d0a0e94 100644 --- a/core/ordtype.v +++ b/core/ordtype.v @@ -86,12 +86,6 @@ Definition oleq (T : ordType) (t1 t2 : T) := ord t1 t2 || (t1 == t2). Prenex Implicits ord oleq. -(* Remove when dropping the compatibility with MathComp 1.11.0: *) -Local Lemma irr_sorted_eq (T : eqType) (leT : rel T) : - transitive leT -> irreflexive leT -> - forall s1 s2 : seq T, sorted leT s1 -> sorted leT s2 -> s1 =i s2 -> s1 = s2. -Proof. by [exact: irr_sorted_eq | exact: eq_sorted_irr]. Qed. - Section Lemmas. Variable T : ordType. Implicit Types x y : T. diff --git a/core/pred.v b/core/pred.v index e95149a..ac55772 100644 --- a/core/pred.v +++ b/core/pred.v @@ -293,7 +293,7 @@ Hint Resolve EqPredType_refl SubPredType_refl : core. (* to reprove the lemmas on refl, sym and trans. *) Add Parametric Relation T (pT : PredType T) : pT (@EqPredType _ pT) - reflexivity proved by (@EqPredType_refl _ _) + reflexivity proved by (@EqPredType_refl _ _) symmetry proved by (@EqPredType_sym _ _) transitivity proved by (@EqPredType_trans' _ _) as EqPredType_rel.