add deprecation warnings for Int31

coq · Jun 15, 2023 · ebbdb41 · ebbdb41
1 parent ba574c6
commit ebbdb41
Show file tree

Hide file tree

Showing 5 changed files with 257 additions and 1 deletion.
diff --git a/doc/changelog/11-standard-library/17734-warn-Int31.rst b/doc/changelog/11-standard-library/17734-warn-Int31.rst
@@ -0,0 +1,6 @@
+- **Deprecated:** :g: Deprecation warnings are now generated for
+  :g:`Numbers.Cyclic.Int31.Cyclic31`, :g:`NNumbers.Cyclic.Int31.Int31`, and
+  :g:`NNumbers.Cyclic.Int31.Ring31`. These modules have been deprecated since
+  Coq 8.10. The modules under :g:`Numbers.Cyclic.Int63` remain available
+  (`#17734 <https://github.com/coq/coq/pull/17734>`_,
+  by Andres Erbsen).
diff --git a/test-suite/output/Int31NumberSyntax.v b/test-suite/output/Int31NumberSyntax.v
@@ -1,5 +1,5 @@
 Require Import Int31 Cyclic31.
-
+Local Set Warnings "-deprecated".
 Open Scope int31_scope.
 Check I31. (* Would be nice to have I31 : digits->digits->...->int31
               For the moment, I31 : digits31 int31, which is better