Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]

Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot

2 files changed, 15 insertions, 2 deletions

diff --git a/doc/changelog/02-specification-language/11600-uniform-syntax.rst b/doc/changelog/02-specification-language/11600-uniform-syntax.rst
new file mode 100644
index 0000000000..3fa3f80301
--- /dev/null
+++ b/doc/changelog/02-specification-language/11600-uniform-syntax.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  New syntax :g:`Inductive Acc A R | x : Prop := ...` to specify which
+  parameters of an inductive are uniform.
+  (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 721c7a7a51..7ce4538a4d 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1063,8 +1063,17 @@ Parameterized inductive types
         | cons3 : A -> list3 -> list3.
         End list3.
 
-     Attributes ``uniform`` and ``nonuniform`` respectively enable and
-     disable uniform parameters for a single inductive declaration block.
+     For finer control, you can use a ``|`` between the uniform and
+     the non-uniform parameters:
+
+     .. coqtop:: in reset
+
+        Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop
+          := Acc_in : (forall y, R y x -> Acc y) -> Acc x.
+
+     The flag can then be seen as deciding whether the ``|`` is at the
+     beginning (when the flag is unset) or at the end (when it is set)
+     of the parameters when not explicitly given.
 
 .. seealso::
    Section :ref:`inductive-definitions` and the :tacn:`induction` tactic.