drop unused compat lemma

imdea-software · Nov 17, 2021 · d68bef5 · d68bef5
1 parent 895c80d
commit d68bef5
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 7 deletions.
diff --git 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
@@ -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.