use RelationClasses instead of Relations_1 in Sorting

Author: andres-erbsen

.nix/rocq-overlays/stdlib-subcomponents/default.nix

@@ -33,7 +33,7 @@ let
     "classical-logic" = [ "arith" ];
     "sets" = [ "classical-logic" ];
     "vectors" = [ "lists" ];
-    "sorting" = [ "lia" "sets" "vectors" ];
+    "sorting" = [ "lia" "vectors" ];
     "orders-ex" = [ "strings" "sorting" ];
     "unicode" = [ ];
     "primitive-int" = [ "unicode" "zarith" ];

doc/stdlib/depends.dot

@@ -39,7 +39,6 @@ digraph stdlib_deps {
 	"orders-ex" -> sorting;
 	sets -> "classical-logic";
 	sorting -> lia;
-	sorting -> sets;
 	sorting -> vectors;
 	"primitive-floats" -> "primitive-int";
 	wellfounded -> lists;

theories/Sorting/Sorted.v

@@ -20,7 +20,7 @@
   The two notions are equivalent if the order is transitive.
 *)
 
-From Stdlib Require Import List Relations Relations_1.
+From Stdlib Require Import List Relations RelationClasses.
 
 (* Set Universe Polymorphism. *)
 
@@ -29,7 +29,7 @@ From Stdlib Require Import List Relations Relations_1.
 Set Implicit Arguments.
 Local Notation "[ ]" := nil (at level 0).
 Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0).
-Arguments Transitive [U] R.
+Local Arguments Transitive [_] R.
 
 Section defs.