New syntax [Inductive Acc A R | x : Prop := ...]

to control uniform parameters.

This replaces the attribute.

2 files changed, 16 insertions, 0 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 09090ce89a..7ce4538a4d 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1063,6 +1063,18 @@ Parameterized inductive types
         | cons3 : A -> list3 -> list3.
         End list3.
 
+     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.