2 files changed, 34 insertions, 7 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8fbd2ea4e7..509ac92f81 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1349,7 +1349,7 @@ folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding
 to invalid |Coq| identifiers are skipped, and, by convention,
 subdirectories named ``CVS`` or ``_darcs`` are skipped too.
 
-Thanks to this mechanism, .vo files are made available through the
+Thanks to this mechanism, ``.vo`` files are made available through the
 logical name of the folder they are in, extended with their own
 basename. For example, the name associated to the file
 ``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for
@@ -1360,17 +1360,17 @@ wrong loadpath afterwards.
 Some folders have a special status and are automatically put in the
 path. |Coq| commands associate automatically a logical path to files in
 the repository trees rooted at the directory from where the command is
-launched, coqlib/user-contrib/, the directories listed in the
-`$COQPATH`, `${XDG_DATA_HOME}/coq/` and `${XDG_DATA_DIRS}/coq/`
-environment variables (see`http://standards.freedesktop.org/basedir-
-spec/basedir-spec-latest.html`_) with the same physical-to-logical
-translation and with an empty logical prefix.
+launched, ``coqlib/user-contrib/``, the directories listed in the
+``$COQPATH``, ``${XDG_DATA_HOME}/coq/`` and ``${XDG_DATA_DIRS}/coq/``
+environment variables (see `XDG base directory specification
+<http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html>`_)
+with the same physical-to-logical translation and with an empty logical prefix.
 
 The command line option ``-R`` is a variant of ``-Q`` which has the strictly
 same behavior regarding loadpaths, but which also makes the
 corresponding ``.vo`` files available through their short names in a way
 not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R`` `path` ``Lib``
-associates to the ``filepath/fOO/Bar/File.vo`` the logical name
+associates to the file path `path`\ ``/path/fOO/Bar/File.vo`` the logical name
 ``Lib.fOO.Bar.File``, but allows this file to be accessed through the
 short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with
 identical base name are present in different subdirectories of a
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index c26ae2a93b..e136252863 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -38,6 +38,7 @@ At the end, the notation “``[entry sep … sep entry]``” stands for a
 possibly empty sequence of expressions parsed by the “``entry``” entry,
 separated by the literal “``sep``”.
 
+.. _lexical-conventions:
 
 Lexical conventions
 ===================
@@ -905,6 +906,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.