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

to control uniform parameters.

This replaces the attribute.

1 files changed, 12 insertions, 0 deletions

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.