Merge PR #11261: Use implicit types for printing (granting wish #10366).

Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego

2 files changed, 12 insertions, 0 deletions

diff --git a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst
new file mode 100644
index 0000000000..51818c666b
--- /dev/null
+++ b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  :cmd:`Implicit Types` are now taken into account for printing. To inhibit it,
+  unset the :flag:`Printing Use Implicit Types` flag
+  (`#11261 <https://github.com/coq/coq/pull/11261>`_,
+  by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index f0bbaed8f3..9686500a35 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2208,6 +2208,13 @@ or :g:`m` to the type :g:`nat` of natural numbers).
 
   Adds blocks of implicit types with different specifications.
 
+.. flag:: Printing Use Implicit Types
+
+  By default, the type of bound variables is not printed when
+  the variable name is associated to an implicit type which matches the
+  actual type of the variable. This feature can be deactivated by
+  turning this flag off.
+
 .. _implicit-generalization:
 
 Implicit generalization