deprecate Rtauto

Author: andres-erbsen

doc/changelog/05-deprecated/161-HEAD.rst

@@ -0,0 +1,7 @@
+- in `Rtauto and rtauto.Bintree`
+
+  + If you use this plugin and would like to continue using it, please open an
+    issue to discuss its maintainership
+    (`#161 <https://github.com/coq/stdlib/pull/161>`_,
+    by Andres Erbsen).
+

doc/stdlib/depends.dot

@@ -60,8 +60,6 @@ digraph stdlib_deps {
 	"primitive-array" -> "primitive-int";
 	streams -> logic;
 	funind -> "arith-base";
-	rtauto -> positive;
-	rtauto -> lists;
 	compat -> zmod;
 	compat -> reals;
 	compat -> "fmaps-fsets-msets";
@@ -70,6 +68,5 @@ digraph stdlib_deps {
 	compat -> extraction;
 	compat -> streams;
 	compat -> funind;
-	compat -> rtauto;
         all -> compat
 }

theories/rtauto/Bintree.v

@@ -7,6 +7,7 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
+Attributes deprecated(since="9.1", note="If you would like to take over maintenance of rtauto, please open an issue.").
 
 From Stdlib Require Export List.
 From Stdlib Require Export BinPos.

theories/rtauto/Rtauto.v

@@ -7,7 +7,8 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
-
+Attributes deprecated(since="9.1", note="Use lia. If you would like to take over maintenance of rtauto, please open an issue.").
+Local Set Warnings "-deprecated".
 
 From Stdlib Require Export List.
 From Stdlib Require Export Bintree.