Document option Uniform Inductive Parameters

2 files changed, 29 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 75f4df06a..886216724 100644
--- a/CHANGES
+++ b/CHANGES
@@ -52,6 +52,9 @@ Vernacular Commands
 - Nested proofs may be enabled through the option `Nested Proofs Allowed`.
   By default, they are disabled and produce an error. The deprecation
   warning which used to occur when using nested proofs has been removed.
+- Added option Uniform Inductive Parameters which abstracts over parameters
+  before typechecking constructors, allowing to write for example
+  `Inductive list (A : Type) := nil : list | cons : A -> list -> list.`
 
 Coq binaries and process model
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index c26ae2a93..56c8aac94 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -905,6 +905,32 @@ Parametrized inductive types
      sort for the inductive definition and will produce a less convenient
      rule for case elimination.
 
+.. opt:: Uniform Inductive Parameters
+
+     When this option is set (it is off by default),
+     inductive definitions are abstracted over their parameters
+     before typechecking constructors, allowing to write:
+
+     .. coqtop:: all undo
+
+        Set Uniform Inductive Parameters.
+        Inductive list3 (A:Set) : Set :=
+        | nil3 : list3
+        | cons3 : A -> list3 -> list3.
+
+     This behavior is essentially equivalent to starting a new section
+     and using :cmd:`Context` to give the uniform parameters, like so
+     (cf. :ref:`section-mechanism`):
+
+     .. coqtop:: all undo
+
+        Section list3.
+        Context (A:Set).
+        Inductive list3 : Set :=
+        | nil3 : list3
+        | cons3 : A -> list3 -> list3.
+        End list3.
+
 .. seealso::
    Section :ref:`inductive-definitions` and the :tacn:`induction` tactic.