From 58d7a14febb1b0ea46ea139f7d695fa42a8222d5 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Wed, 18 Dec 2019 15:40:41 +0100
Subject: Correct manual about implicit parameters in inductives.

---
 doc/sphinx/language/gallina-extensions.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 78428be18f..005f01b92a 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1629,8 +1629,8 @@ The syntax is supported in all top-level definitions:
 :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype
 declarations, the semantics are the following: an inductive parameter
 declared as an implicit argument need not be repeated in the inductive
-definition but will become implicit for the constructors of the
-inductive only, not the inductive type itself. For example:
+definition and will become implicit for the inductive type and the constructors.
+For example:
 
 .. coqtop:: all
 
-- 
cgit v1.2.3