From 59d8aea2665828619d42a012ec1650ccac5c4c94 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 13 Mar 2019 09:51:25 +0100
Subject: [refman] Remove warning silencing by fixing the underlying issue.

---
 doc/sphinx/language/gallina-extensions.rst | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index a728f5ba02..c87d197179 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1713,19 +1713,15 @@ of constants. For instance, the variable ``p`` below has type
 ``forall x,y:U, R x y -> forall z:U, R y z -> R x z``. As the variables ``x``, ``y`` and ``z``
 appear strictly in the body of the type, they are implicit.
 
-.. coqtop:: reset none
-
-   Set Warnings "-local-declaration".
-
 .. coqtop:: all
 
-   Variable X : Type.
+   Parameter X : Type.
 
    Definition Relation := X -> X -> Prop.
 
    Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z.
 
-   Variables (R : Relation) (p : Transitivity R).
+   Parameters (R : Relation) (p : Transitivity R).
 
    Arguments p : default implicits.
 
@@ -1733,7 +1729,7 @@ appear strictly in the body of the type, they are implicit.
 
    Print Implicit p.
 
-   Variables (a b c : X) (r1 : R a b) (r2 : R b c).
+   Parameters (a b c : X) (r1 : R a b) (r2 : R b c).
 
    Check (p r1 r2).
 
-- 
cgit v1.2.3