From 890f206ebea4a14f5be8b273cee4ae8f99ca25e1 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 19 Apr 2019 18:52:26 +0200 Subject: Split changes between main changes and other changes (no repetition). Add more links to PRs and credits of authors. --- doc/sphinx/user-extensions/syntax-extensions.rst | 2 ++ 1 file changed, 2 insertions(+) (limited to 'doc/sphinx/user-extensions') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 3ca1dda4d6..ac079ea7d5 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1376,6 +1376,8 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. +.. _numeral-notations: + Numeral notations ----------------- -- cgit v1.2.3 From beb5bdec79ff371f48a478df3c24f2cf9d68aa1f Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Tue, 7 May 2019 15:04:04 -0700 Subject: Use Print Custom Grammar to inspect custom entries --- doc/sphinx/user-extensions/syntax-extensions.rst | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'doc/sphinx/user-extensions') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ac079ea7d5..edec13f681 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -840,10 +840,11 @@ gives a way to let any arbitrary expression which is not handled by the custom entry ``expr`` be parsed or printed by the main grammar of term up to the insertion of a pair of curly brackets. -.. cmd:: Print Grammar @ident. +.. cmd:: Print Custom Grammar @ident. + :name: Print Custom Grammar - This displays the state of the grammar for terms and grammar for - patterns associated to the custom entry :token:`ident`. + This displays the state of the grammar for terms associated to + the custom entry :token:`ident`. Summary ~~~~~~~ -- cgit v1.2.3 From 942621f7747bd56a7da35cacc21f0e5fdbf93413 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Sun, 12 May 2019 19:38:36 -0400 Subject: [refman] Misc fixes (indentation, whitespace, notation syntax) --- doc/sphinx/user-extensions/proof-schemes.rst | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) (limited to 'doc/sphinx/user-extensions') diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 418922e9b3..3a12ee288a 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -336,29 +336,32 @@ Generation of induction principles with ``Functional`` ``Scheme`` Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- -.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort +.. cmd:: Derive Inversion @ident with @ident Sort @sort + Derive Inversion @ident with (forall @binders, @ident @term) Sort @sort This command generates an inversion principle for the - :tacn:`inversion ... using ...` tactic. Let :g:`I` be an inductive - predicate and :g:`x` the variables occurring in t. This command - generates and stocks the inversion lemma for the sort :g:`sort` - corresponding to the instance :g:`∀ (x:T), I t` with the name - :n:`@ident` in the global environment. When applied, it is - equivalent to having inverted the instance with the tactic - :g:`inversion`. - + :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name + of the generated principle. The second :token:`ident` should be an inductive + predicate, and :token:`binders` the variables occurring in the term + :token:`term`. This command generates the inversion lemma for the sort + :token:`sort` corresponding to the instance :n:`forall @binders, @ident @term`. + When applied, it is equivalent to having inverted the instance with the + tactic :g:`inversion`. -.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort @sort +.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort + Derive Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic `inversion_clear`. -.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort @sort +.. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort + Derive Dependent Inversion @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion`. -.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort @sort +.. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort + Derive Dependent Inversion_clear @ident with (forall @binders, @ident @term) Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion_clear`. -- cgit v1.2.3 From 2a4bd4861d0ebf0b5d5a63774ac964b431e94fbb Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 16 May 2019 10:59:33 -0400 Subject: [refman] Add a .. cmd:: header for Reserved Notation and Reserved Infix Co-Authored-By: Théo Zimmermann --- doc/sphinx/user-extensions/syntax-extensions.rst | 31 +++++++++++++++--------- 1 file changed, 19 insertions(+), 12 deletions(-) (limited to 'doc/sphinx/user-extensions') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index edec13f681..cda228a7da 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -327,22 +327,29 @@ symbols. Reserving notations ~~~~~~~~~~~~~~~~~~~ -A given notation may be used in different contexts. Coq expects all -uses of the notation to be defined at the same precedence and with the -same associativity. To avoid giving the precedence and associativity -every time, it is possible to declare a parsing rule in advance -without giving its interpretation. Here is an example from the initial -state of Coq. +.. cmd:: Reserved Notation @string {? (@modifiers) } -.. coqtop:: in + A given notation may be used in different contexts. Coq expects all + uses of the notation to be defined at the same precedence and with the + same associativity. To avoid giving the precedence and associativity + every time, this command declares a parsing rule (:token:`string`) in advance + without giving its interpretation. Here is an example from the initial + state of Coq. + + .. coqtop:: in + + Reserved Notation "x = y" (at level 70, no associativity). + + Reserving a notation is also useful for simultaneously defining an + inductive type or a recursive constant and a notation for it. - Reserved Notation "x = y" (at level 70, no associativity). + .. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence + their precedence and associativity cannot be changed. -Reserving a notation is also useful for simultaneously defining an -inductive type or a recursive constant and a notation for it. + .. cmdv:: Reserved Infix "@symbol" {* @modifiers} -.. note:: The notations mentioned in the module :ref:`init-notations` are reserved. Hence - their precedence and associativity cannot be changed. + This command declares an infix parsing rule without giving its + interpretation. Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3