document deprecation of relations

Author: andres-erbsen

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

@@ -11,7 +11,7 @@ let
     "logic" = [ ];
     "relations" = [ "corelib-wrapper" ];
     "program" = [ "corelib-wrapper" "logic" ];
-    "classes" = [ "program" "relations" ];
+    "classes" = [ "program" ];
     "bool" = [ "classes" ];
     "structures" = [ "bool" ];
     "arith-base" = [ "structures" ];
@@ -34,7 +34,7 @@ let
     "classical-logic" = [ "arith" ];
     "sets" = [ "classical-logic" ];
     "vectors" = [ "lists" ];
-    "sorting" = [ "lia" "sets" "vectors" ];
+    "sorting" = [ "lia" "sets" "vectors" "relations"]];
     "orders-ex" = [ "strings" "sorting" ];
     "unicode" = [ ];
     "primitive-int" = [ "unicode" "zarith" ];
@@ -45,7 +45,7 @@ let
     "fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
     "extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
     "funind" = [ "arith-base" ];
-    "wellfounded" = [ "lists" ];
+    "wellfounded" = [ "relations" "lists" ];
     "streams" = [ "logic" ];
     "rtauto" = [ "positive" "lists" ];
     "compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "zmod" "wellfounded" "streams" ];

doc/changelog/01-changed/162-deprecate-relations.rst

@@ -0,0 +1,6 @@
+- in `Wellfounded`
+
+  + Changed definitions to use `RelationClasses` instead of `Relations`
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+

doc/changelog/05-deprecated/162-deprecate-relations.rst

@@ -0,0 +1,18 @@
+- in `Relation_Definitions`
+
+  + Everything except `relation`, in favor of `RelationClasses`
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+
+- in `Relations`
+
+  + All uses of `Relations`, adding `RelationClasses` versions
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+
+- in `Operators_Properties`
+
+  + All uses of `Relation_Definitions`, adding `RelationClasses` versions
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+

doc/stdlib/depends.dot

@@ -9,7 +9,8 @@ digraph stdlib_deps {
 	];
 	bool -> classes;
 	classes -> program;
-	classes -> relations;
+	wellfounded -> relations;
+	sorting -> relations;
 	program -> "corelib-wrapper";
 	program -> logic;
 	strings -> arith;