From 36e38a3768251dbcf20c4de2b746e5eee33da909 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:12:10 -0400 Subject: [doc] Use productionlist instead of prodn in ring.rst --- doc/sphinx/addendum/ring.rst | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 47d3a7d7cd..6a9b343ba8 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -310,16 +310,15 @@ The :n:`@ident` is not relevant. It is just used for error messages. The axioms. The optional list of modifiers is used to tailor the behavior of the tactic. The following list describes their syntax and effects: -.. prodn:: - ring_mod ::= abstract %| decidable @term %| morphism @term - %| setoid @term @term - %| constants [@ltac] - %| preprocess [@ltac] - %| postprocess [@ltac] - %| power_tac @term [@ltac] - %| sign @term - %| div @term - +.. productionlist:: coq + ring_mod : abstract | decidable `term` | morphism `term` + : | setoid `term` `term` + : | constants [`ltac`] + : | preprocess [`ltac`] + : | postprocess [`ltac`] + : | power_tac `term` [`ltac`] + : | sign `term` + : | div `term` abstract declares the ring as abstract. This is the default. @@ -663,8 +662,8 @@ messages. :n:`@term` is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is used to tailor the behavior of the tactic. -.. prodn:: - field_mod := @ring_mod %| completeness @term +.. productionlist:: coq + field_mod : `ring_mod` | completeness `term` Since field tactics are built upon ``ring`` tactics, all modifiers of the ``Add Ring`` apply. There is only one -- cgit v1.2.3 From 4687e40504024b51b63bc5681feba13ea6dffbaf Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:09:26 -0400 Subject: [doc] Fix uncaught duplicate-label errors in the SSReflect chapter --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1c554acdb8..16d0420ec8 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2402,7 +2402,7 @@ tactic: The behavior of the defective have tactic makes it possible to generalize it in the following general construction: -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @binder } } {? : @term } {? := @term | by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic } Open syntax is supported for both :token:`term`. For the description of :token:`i_item` and :token:`s_item` see section @@ -5242,7 +5242,7 @@ Notation scope Module name -.. prodn:: name ::= @qualid +.. prodn:: modname ::= @qualid Natural number @@ -5252,14 +5252,10 @@ where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral (should not be the name of a tactic which can be followed by a bracket ``[``, like ``do``, ``have``,…) -Pattern - -.. prodn:: pattern ::= @term - Items and switches ~~~~~~~~~~~~~~~~~~ -.. prodn:: binder ::= @ident %| ( @ident {? : @term } ) +.. prodn:: ssr_binder ::= @ident %| ( @ident {? : @term } ) binder see :ref:`abbreviations_ssr`. @@ -5354,8 +5350,8 @@ case analysis see :ref:`the_defective_tactics_ssr` rewrite see :ref:`rewriting_ssr` -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } {? : @term } := @term -.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } : @term {? by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term +.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } .. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term .. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } .. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } @@ -5369,9 +5365,9 @@ forward chaining see :ref:`structure_ssr` specializing see :ref:`structure_ssr` -.. tacn:: suff {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } +.. tacn:: suff {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } :name: suff -.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } +.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } :name: suffices .. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } .. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } @@ -5382,7 +5378,7 @@ backchaining see :ref:`structure_ssr` local definition :ref:`definitions_ssr` -.. tacv:: pose @ident {+ @binder } := @term +.. tacv:: pose @ident {+ @ssr_binder } := @term local function definition -- cgit v1.2.3 From 21a0af5b7743e5a1013438210492991b51d878c4 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:09:06 -0400 Subject: [doc] Fix a typo in the ssreflect chapter --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 16d0420ec8..ab52c2ce78 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1484,7 +1484,7 @@ The abstract tactic ``````````````````` .. tacn:: abstract: {+ d_item} - :name abstract (ssreflect) + :name: abstract (ssreflect) This tactic assigns an abstract constant previously introduced with the ``[: name ]`` intro pattern (see section :ref:`introduction_ssr`). -- cgit v1.2.3 From 3d8342c2c26f710583e6b9246bd1069cb8b42d7d Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:10:15 -0400 Subject: [doc] Rewrite and document the prodn directive It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place. --- doc/sphinx/README.rst | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 35a605ddd3..32de15ee31 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -123,11 +123,24 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the induction principles. -``.. prodn::`` :black_nib: Grammar productions. +``.. prodn::`` A grammar production. This is useful if you intend to document individual grammar productions. Otherwise, use Sphinx's `production lists `_. + Unlike ``.. productionlist``\ s, this directive accepts notation syntax. + + + Usage:: + + .. prodn:: token += production + .. prodn:: token ::= production + + Example:: + + .. prodn:: term += let: @pattern := @term in @term + .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + ``.. tacn::`` :black_nib: A tactic, or a tactic notation. Example:: -- cgit v1.2.3