From a249cc95c1345442c67e240e881fb653579ee386 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 12 Mar 2019 21:48:04 +0100 Subject: [refman] Add 'warn' option to coqtop directive. Fix semantic conflict between #9389 and #9654. --- doc/sphinx/language/gallina-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8b7e5c9a02..b59d0bb723 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1655,7 +1655,7 @@ Declaring Implicit Arguments For instance in - .. coqtop:: all + .. coqtop:: all warn Arguments prod _ [_]. -- cgit v1.2.3 From 6c20e7d284280d7c3927aab6ea9b46b86998a00e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 Mar 2019 09:48:17 +0100 Subject: [refman] Fix other newly emitted warnings. --- doc/sphinx/addendum/extended-pattern-matching.rst | 2 +- doc/sphinx/language/gallina-extensions.rst | 10 ++++++---- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 3ec6c118af..e882ce6e88 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -285,7 +285,7 @@ By default, implicit arguments are omitted in patterns. So we write: .. coqtop:: all - Arguments nil [A]. + Arguments nil {A}. Arguments cons [A] _ _. Check (fun l:List nat => diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index b59d0bb723..a728f5ba02 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1621,7 +1621,7 @@ Declaring Implicit Arguments .. coqtop:: reset all - Inductive list (A:Type) : Type := + Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. @@ -1629,13 +1629,15 @@ Declaring Implicit Arguments Arguments cons [A] _ _. - Arguments nil [A]. + Arguments nil {A}. Check (cons 3 nil). - Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B := match l with nil => nil | cons a t => cons (f a) (map A B f t) end. + Fixpoint map (A B : Type) (f : A -> B) (l : list A) : list B := + match l with nil => nil | cons a t => cons (f a) (map A B f t) end. - Fixpoint length (A:Type) (l:list A) : nat := match l with nil => 0 | cons _ m => S (length A m) end. + Fixpoint length (A : Type) (l : list A) : nat := + match l with nil => 0 | cons _ m => S (length A m) end. Arguments map [A B] f l. -- cgit v1.2.3 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(-) 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 From 1eb1fe7cee6f8381c5c715430eba0c5994f0b3a4 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 Mar 2019 09:54:28 +0100 Subject: [refman] Fix Sphinx-translation regression in Arguments command. --- doc/sphinx/language/gallina-extensions.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c87d197179..59506a6ff2 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1575,7 +1575,7 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* [ @ident ] | @ident } +.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, @@ -1592,20 +1592,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* [ @ident ] | @ident } +.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* [ @ident ] | @ident } +.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | @ident } } +.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of -- cgit v1.2.3