diff options
| author | Théo Zimmermann | 2019-03-13 09:51:25 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-13 09:51:25 +0100 |
| commit | 59d8aea2665828619d42a012ec1650ccac5c4c94 (patch) | |
| tree | 2d9b844b94e25ced6e12f1bb18ea197f31590fdf | |
| parent | 6c20e7d284280d7c3927aab6ea9b46b86998a00e (diff) | |
[refman] Remove warning silencing by fixing the underlying issue.
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 10 |
1 files changed, 3 insertions, 7 deletions
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). |