diff options
Diffstat (limited to 'doc')
23 files changed, 9547 insertions, 141 deletions
diff --git a/doc/changelog/02-specification-language/10441-static-poly-section.rst b/doc/changelog/02-specification-language/10441-static-poly-section.rst new file mode 100644 index 0000000000..7f0345d946 --- /dev/null +++ b/doc/changelog/02-specification-language/10441-static-poly-section.rst @@ -0,0 +1,11 @@ +- The universe polymorphism setting now applies from the opening of a section. + In particular, it is not possible anymore to mix polymorphic and monomorphic + definitions in a section when there are no variables nor universe constraints + defined in this section. This makes the behaviour consistent with the + documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_, + by Pierre-Marie Pédrot) + +- The :cmd:`Section` vernacular command now accepts the "universes" attribute. In + addition to setting the section universe polymorphism, it also locally sets + the universe polymorphic option inside the section. + (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) diff --git a/doc/changelog/08-tools/10430-extraction-int63.rst b/doc/changelog/08-tools/10430-extraction-int63.rst new file mode 100644 index 0000000000..68ae4591a4 --- /dev/null +++ b/doc/changelog/08-tools/10430-extraction-int63.rst @@ -0,0 +1,5 @@ +- Fix extraction to OCaml of primitive machine integers; + see :ref:`primitive-integers` + (`#10430 <https://github.com/coq/coq/pull/10430>`_, + fixes `#10361 <https://github.com/coq/coq/issues/10361>`_, + by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst new file mode 100644 index 0000000000..ab625b9e03 --- /dev/null +++ b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst @@ -0,0 +1,4 @@ +- Removes deprecated modules `Coq.ZArith.Zlogarithm` + and `Coq.ZArith.Zsqrt_compat` + (#9881 <https://github.com/coq/coq/pull/9811> + by Vincent Laporte). diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 3f4d5cc784..1098aa75da 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -76,7 +76,7 @@ an arbitrary order: ===== =============== ========================= Then normalize the “abstract” polynomial -:math:`((V_1 \otimes V_2 ) \oplus V_2) \oplus (V_0 \otimes 2)` +:math:`((V_1 \oplus V_2 ) \otimes V_2) \oplus (V_0 \otimes 2)` In our example the normal form is: :math:`(2 \otimes V_0 ) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2 )`. Then substitute the variables by their values in the variables map to diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 395b5ce2d3..7e698bfb66 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -144,6 +144,8 @@ Many other commands support the ``Polymorphic`` flag, including: - ``Lemma``, ``Axiom``, and all the other “definition” keywords support polymorphism. +- :cmd:`Section` will locally set the polymorphism flag inside the section. + - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support polymorphism. This means that the universe variables (and associated constraints) are discharged polymorphically over definitions that use diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index fd84868a1f..6ac55e7bf4 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -102,10 +102,10 @@ reference manual. Here are the most important user-visible changes: extensionality lemma: - interactive mode: :n:`under @term`, associated terminator: :tacn:`over` - - one-liner mode: `under @term do [@tactic | ...]` + - one-liner mode: :n:`under @term do [@tactic | ...]` It can take occurrence switches, contextual patterns, and intro patterns: - :g:`under {2}[in RHS]eq_big => [i|i ?] do ...` + :g:`under {2}[in RHS]eq_big => [i|i ?]` (`#9651 <https://github.com/coq/coq/pull/9651>`_, by Erik Martin-Dorel and Enrico Tassi). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index d1b95e6203..ac75240cfb 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -7,22 +7,20 @@ The |Coq| library single: Theories -The |Coq| library is structured into two parts: +The |Coq| library has two parts: - * **The initial library**: it contains elementary logical notions and - data-types. It constitutes the basic state of the system directly - available when running |Coq|; + * **The basic library**: definitions and theorems for + the most commonly used elementary logical notions and + data types. |Coq| normally loads these files automatically when it starts. - * **The standard library**: general-purpose libraries containing various - developments of |Coq| axiomatizations about sets, lists, sorting, - arithmetic, etc. This library comes with the system and its modules - are directly accessible through the ``Require`` command (see - Section :ref:`compiled-files`); + * **The standard library**: general-purpose libraries with + definitions and theorems for sets, lists, sorting, + arithmetic, etc. To use these files, users must load them explicitly + with the ``Require`` command (see :ref:`compiled-files`) -In addition, user-provided libraries or developments are provided by -|Coq| users' community. These libraries and developments are available -for download at http://coq.inria.fr (see -Section :ref:`userscontributions`). +There are also many libraries provided by |Coq| users' community. +These libraries and developments are available +for download at http://coq.inria.fr (see :ref:`userscontributions`). This chapter briefly reviews the |Coq| libraries whose contents can also be browsed at http://coq.inria.fr/stdlib. @@ -514,8 +512,8 @@ realizability interpretation. forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P. -Basic Arithmetics -~~~~~~~~~~~~~~~~~ +Basic Arithmetic +~~~~~~~~~~~~~~~~ The basic library includes a few elementary properties of natural numbers, together with the definitions of predecessor, addition and @@ -804,8 +802,8 @@ Notation Interpretation =============== =================== -Notations for integer arithmetics -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Notations for integer arithmetic +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. index:: single: Arithmetical notations @@ -822,7 +820,7 @@ Notations for integer arithmetics The following table describes the syntax of expressions -for integer arithmetics. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``. +for integer arithmetic. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``. It specifies how notations are interpreted and, when not already reserved, the precedence and associativity. @@ -866,7 +864,7 @@ Notations for real numbers This is provided by requiring and opening the module ``Reals`` and opening scope ``R_scope``. This set of notations is very similar to -the notation for integer arithmetics. The inverse function was added. +the notation for integer arithmetic. The inverse function was added. =============== =================== Notation Interpretation diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c93984661e..acf68e9fd2 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2443,12 +2443,19 @@ The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement dedicated, efficient, rules to reduce the applications of these primitive operations. -These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to -types and functions of a :g:`Uint63` module. Said module is not produced by +The extraction of these primitives can be customized similarly to the extraction +of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` +module can be used when extracting to OCaml: it maps the Coq primitives to types +and functions of a :g:`Uint63` module. Said OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq. +Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values +wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on +64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the +function :g:`Uint63.compile` from the kernel). + Bidirectionality hints ---------------------- diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 38f6714f46..91dfa34494 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -44,78 +44,91 @@ Lexical conventions =================== Blanks - Space, newline and horizontal tabulation are considered as blanks. + Space, newline and horizontal tab are considered blanks. Blanks are ignored but they separate tokens. Comments - Comments in Coq are enclosed between ``(*`` and ``*)``, and can be nested. - They can contain any character. However, :token:`string` literals must be + Comments are enclosed between ``(*`` and ``*)``. They can be nested. + They can contain any character. However, embedded :token:`string` literals must be correctly closed. Comments are treated as blanks. -Identifiers and access identifiers +Identifiers and field identifiers Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and - ``'``, that do not start with a digit or ``'``. That is, they are - recognized by the following lexical class: + ``'``, that do not start with a digit or ``'``. That is, they are + recognized by the following grammar (except that the string ``_`` is reserved; + it is not a valid identifier): .. productionlist:: coq - first_letter : a..z ∣ A..Z ∣ _ ∣ unicode-letter - subsequent_letter : a..z ∣ A..Z ∣ 0..9 ∣ _ ∣ ' ∣ unicode-letter ∣ unicode-id-part ident : `first_letter`[`subsequent_letter`…`subsequent_letter`] - access_ident : .`ident` + field : .`ident` + first_letter : a..z ∣ A..Z ∣ _ ∣ `unicode_letter` + subsequent_letter : `first_letter` ∣ 0..9 ∣ ' ∣ `unicode_id_part` All characters are meaningful. In particular, identifiers are case-sensitive. - The entry ``unicode-letter`` non-exhaustively includes Latin, + :production:`unicode_letter` non-exhaustively includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical letter-like - symbols, hyphens, non-breaking space, … The entry ``unicode-id-part`` + symbols and non-breaking space. :production:`unicode_id_part` non-exhaustively includes symbols for prime letters and subscripts. - Access identifiers, written :token:`access_ident`, are identifiers prefixed by - `.` (dot) without blank. They are used in the syntax of qualified - identifiers. + Field identifiers, written :token:`field`, are identifiers prefixed by + `.` (dot) with no blank between the dot and the identifier. They are used in + the syntax of qualified identifiers. Numerals - Numerals are sequences of digits with a potential fractional part - and exponent. Integers are numerals without fractional nor exponent - part and optionally preceded by a minus sign. Underscores ``_`` can - be used as comments in numerals. + Numerals are sequences of digits with an optional fractional part + and exponent, optionally preceded by a minus sign. :token:`int` is an integer; + a numeral without fractional or exponent parts. :token:`num` is a non-negative + integer. Underscores embedded in the digits are ignored, for example + ``1_000_000`` is the same as ``1000000``. .. productionlist:: coq - digit : 0..9 + numeral : `num`[. `num`][`exp`[`sign`]`num`] + int : [-]`num` num : `digit`…`digit` - integer : [-]`num` - dot : . + digit : 0..9 exp : e | E sign : + | - - numeral : `num`[`dot` `num`][`exp`[`sign`]`num`] Strings - Strings are delimited by ``"`` (double quote), and enclose a sequence of - any characters different from ``"`` or the sequence ``""`` to denote the - double quote character. In grammars, the entry for quoted strings is - :production:`string`. + Strings begin and end with ``"`` (double quote). Use ``""`` to represent + a double quote character within a string. In the grammar, strings are + identified with :production:`string`. Keywords - The following identifiers are reserved keywords, and cannot be - employed otherwise:: - - _ as at cofix else end exists exists2 fix for - forall fun if IF in let match mod return - SProp Prop Set Type then using where with - -Special tokens - The following sequences of characters are special tokens:: - - ! % & && ( () ) * + ++ , - -> . .( .. - / /\ : :: :< := :> ; < <- <-> <: <= <> = - => =_D > >-> >= ? ?= @ [ \/ ] ^ { | |- - || } ~ #[ - - Lexical ambiguities are resolved according to the “longest match” - rule: when a sequence of non alphanumerical characters can be - decomposed into several different ways, then the first token is the - longest possible one (among all tokens defined at this moment), and so - on. + The following character sequences are reserved keywords that cannot be + used as identifiers:: + + _ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop + SProp Set Theorem Type Variable as at by cofix discriminated else + end exists exists2 fix for forall fun if in lazymatch let match + multimatch return then using where with + + Note that plugins may define additional keywords when they are loaded. + +Other tokens + The set of + tokens defined at any given time can vary because the :cmd:`Notation` + command can define new tokens. A :cmd:`Require` command may load more notation definitions, + while the end of a :cmd:`Section` may remove notations. Some notations + are defined in the basic library (see :ref:`thecoqlibrary`) and are normallly + loaded automatically at startup time. + + Here are the character sequences that Coq directly defines as tokens + without using :cmd:`Notation` (omitting 25 specialized tokens that begin with + ``#int63_``):: + + ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> + . .( .. ... / : ::= := :> :>> ; < <+ <- <: + <<: <= = => > >-> >= ? @ @{ [ [= ] _ _eqn + `( `{ { {| | |- || } + + When multiple tokens match the beginning of a sequence of characters, + the longest matching token is used. + Occasionally you may need to insert spaces to separate tokens. For example, + if ``~`` and ``~~`` are both defined as tokens, the inputs ``~ ~`` and + ``~~`` generate different tokens, whereas if `~~` is not defined, then the + two inputs are equivalent. .. _term: @@ -164,7 +177,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : ( `name` [: `term`] := `term` ) : ' `pattern` name : `ident` | _ - qualid : `ident` | `qualid` `access_ident` + qualid : `ident` | `qualid` `field` sort : SProp | Prop | Set | Type fix_bodies : `fix_body` : `fix_body` with `fix_body` with … with `fix_body` for `ident` diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index efb5df720a..7d6171285e 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -88,8 +88,6 @@ There are other buttons on the |CoqIDE| toolbar: a button to save the running buffer; a button to close the current buffer (an "X"); buttons to switch among buffers (left and right arrows); an "information" button; and a "gears" button. -The "information" button is described in Section :ref:`try-tactics-automatically`. - The "gears" button submits proof terms to the |Coq| kernel for type checking. When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), proofs may have been completed without kernel-checking of generated proof terms. @@ -100,27 +98,6 @@ processed color, though their preceding proofs have the processed color. Notice that for all these buttons, except for the "gears" button, their operations are also available in the menu, where their keyboard shortcuts are given. -.. _try-tactics-automatically: - -Trying tactics automatically ------------------------------- - -The menu Try Tactics provides some features for automatically trying -to solve the current goal using simple tactics. If such a tactic -succeeds in solving the goal, then its text is automatically inserted -into the script. There is finally a combination of these tactics, -called the *proof wizard* which will try each of them in turn. This -wizard is also available as a tool button (the "information" button). The set of -tactics tried by the wizard is customizable in the preferences. - -These tactics are general ones, in particular they do not refer to -particular hypotheses. You may also try specific tactics related to -the goal or one of the hypotheses, by clicking with the right mouse -button on the goal or the considered hypothesis. This is the -“contextual menu on goals” feature, that may be disabled in the -preferences if undesirable. - - Proof folding ------------------ @@ -202,13 +179,6 @@ compilation, printing, web browsing. In the browser command, you may use `%s` to denote the URL to open, for example: `firefox -remote "OpenURL(%s)"`. -The `Tactics Wizard` section allows defining the set of tactics that -should be tried, in sequence, to solve the current goal. - -The last section is for miscellaneous boolean settings, such as the -“contextual menu on goals” feature presented in the section -:ref:`Try tactics automatically <try-tactics-automatically>`. - Notice that these settings are saved in the file `.coqiderc` of your home directory. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 46f9826e41..362c3da6cb 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -31,10 +31,10 @@ Syntax The syntax of the tactic language is given below. See Chapter :ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used in these grammar rules. Various already defined entries will be used in this -chapter: entries :token:`natural`, :token:`integer`, :token:`ident`, +chapter: entries :token:`num`, :token:`int`, :token:`ident` :token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic` -represent respectively the natural and integer numbers, the authorized -identificators and qualified names, Coq terms and patterns and all the atomic +represent respectively natural and integer numbers, +identifiers, qualified names, Coq terms, patterns and the atomic tactics described in Chapter :ref:`tactics`. The syntax of :production:`cpattern` is @@ -141,10 +141,10 @@ mode but it can also be used in toplevel definitions as shown below. : `atom` atom : `qualid` : () - : `integer` + : `int` : ( `ltac_expr` ) component : `string` | `qualid` - message_token : `string` | `ident` | `integer` + message_token : `string` | `ident` | `int` tacarg : `qualid` : () : ltac : `atom` @@ -159,11 +159,11 @@ mode but it can also be used in toplevel definitions as shown below. match_rule : `cpattern` => `ltac_expr` : context [`ident`] [ `cpattern` ] => `ltac_expr` : _ => `ltac_expr` - test : `integer` = `integer` - : `integer` (< | <= | > | >=) `integer` + test : `int` = `int` + : `int` (< | <= | > | >=) `int` selector : [`ident`] - : `integer` - : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) + : `int` + : (`int` | `int` - `int`), ..., (`int` | `int` - `int`) toplevel_selector : `selector` : all : par diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 3036648b08..ceaa2775bf 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -179,7 +179,7 @@ constructions from ML. : let `ltac2_var` := `ltac2_term` in `ltac2_term` : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end - : `integer` + : `int` : `string` : `ltac2_term` ; `ltac2_term` : [| `ltac2_term` ; ... ; `ltac2_term` |] @@ -670,7 +670,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression. .. prodn:: - ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) } + ltac2_scope ::= {| @string | @int | @lident ({+, @ltac2_scope}) } A few scopes contain antiquotation features. For sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. @@ -719,7 +719,7 @@ The following scopes are built-in. + parses a Ltac2 expression at the next level and return it as is. -- :n:`tactic(n = @integer)`: +- :n:`tactic(n = @int)`: + parses a Ltac2 expression at the provided level :n:`n` and return it as is. @@ -760,7 +760,7 @@ Notations The Ltac2 parser can be extended by syntactic notations. -.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term +.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @int} := @ltac2_term :name: Ltac2 Notation A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1b9e3ce0f3..ed980bd4de 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3761,10 +3761,10 @@ involves the following steps: 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. - These protected goals are displayed using the ``Under[ … ]`` - notation (e.g. ``Under[ m - m ]`` in the running example). + These protected goals are displayed using the ``'Under[ … ]`` + notation (e.g. ``'Under[ m - m ]`` in the running example). -6. The expression inside the ``Under[ … ]`` notation can be +6. The expression inside the ``'Under[ … ]`` notation can be proved equivalent to the desired expression by using a regular :tacn:`rewrite` tactic. @@ -3782,7 +3782,7 @@ The over tactic Two equivalent facilities (a terminator and a lemma) are provided to close intermediate subgoals generated by :tacn:`under` (i.e. goals -displayed as ``Under[ … ]``): +displayed as ``'Under[ … ]``): .. tacn:: over :name: over @@ -3792,7 +3792,7 @@ displayed as ``Under[ … ]``): .. tacv:: by rewrite over - This is a variant of :tacn:`over` in order to close ``Under[ … ]`` + This is a variant of :tacn:`over` in order to close ``'Under[ … ]`` goals, relying on the ``over`` rewrite rule. .. _under_one_liner: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 5f3e82938d..774732825a 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -870,26 +870,6 @@ interactively, they cannot be part of a vernacular file loaded via have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if necessary. - .. cmdv:: Backtrack @num @num @num - :name: Backtrack - - .. deprecated:: 8.4 - - :cmd:`Backtrack` is a *deprecated* form of - :cmd:`BackTo` which allows explicitly manipulating the proof environment. The - three numbers represent the following: - - + *first number* : State label to reach, as for :cmd:`BackTo`. - + *second number* : *Proof state number* to unbury once aborts have been done. - |Coq| will compute the number of :cmd:`Undo` to perform (see Chapter :ref:`proofhandling`). - + *third number* : Number of :cmd:`Abort` to perform, i.e. the number of currently - opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`). - - .. exn:: Invalid backtrack. - - The destination state label is unknown. - - .. _quitting-and-debugging: Quitting and debugging diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b25104ddb9..46175e37ed 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,6 +12,7 @@ plugins/extraction/ExtrHaskellZInteger.v plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOCamlInt63.v plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 61d601be7d..dcfe4a08f3 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -181,14 +181,12 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zhints.v (theories/ZArith/ZArith_base.v) theories/ZArith/Zcomplements.v - theories/ZArith/Zsqrt_compat.v theories/ZArith/Zpow_def.v theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v theories/ZArith/Zquot.v theories/ZArith/Zeuclid.v - theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) theories/ZArith/Zgcd_alt.v theories/ZArith/Zwf.v diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md new file mode 100644 index 0000000000..98fdc38ca7 --- /dev/null +++ b/doc/tools/docgram/README.md @@ -0,0 +1,208 @@ +# Grammar extraction tool for documentation + +`doc_grammar` extracts Coq's grammar from `.mlg` files, edits it and inserts it in +chunks into `.rst` files. The tool currently inserts Sphinx +`productionlist` constructs. It also generates a file with `prodn` constructs +for the entire grammar, but updates to `tacn` and `cmd` constructs must be done +manually since the grammar doesn't have names for them as it does for +nonterminals. There is an option to report which `tacn` and `cmd` were not +found in the `.rst` files. `tacv` and `cmdv` constructs are not processed at all. + +The mlg grammars present several challenges to generating an accurate grammar +for documentation purposes: + +* The 30+ mlg files don't define an overall order in which nonterminals should + appear in a complete grammar. + +* Even within a single mlg file, nonterminals and productions are often given + in an order that's much different from what a reader of the documentation would + expect. In a small number of cases, changing the order in the mlg would change + how some inputs are parsed, in particular when the order determines how to distinguish + otherwise ambiguous inputs. + + Strictly speaking, that means our grammar is not a context free grammar even though + we gloss over that distinction in the documentation. + +* For a few nonterminals, some productions are only available if certain plugins + are activated (e.g. SSR). Readers should be informed about these. + +* Some limited parts of the grammar are defined in OCaml, including lookahead symbols + like `test_bracket_ident` and references to nonterminals in other files using + qualified names such as `Prim.ident`. A few symbols are defined multiple times, + such as `scope` and `orient`. + +## What the tool does + +1. The tool reads all the `mlg` files and generates `fullGrammar`, which includes +all the grammar without the actions for each production or the OCaml code. This +file is provided as a convenience to make it easier to examine the (mostly) +unprocessed grammar of the mlg files with less clutter. Nonterminals that use +levels (`"5" RIGHTA` below) are modified, for example: + +``` +tactic_expr: + [ "5" RIGHTA + [ te = binder_tactic -> { te } ] +``` + +becomes + +``` +tactic_expr5: [ +| binder_tactic +| tactic_expr4 +] +``` + +2. The tool applies grammar editing operations specified by `common.edit_mlg` to +generate `editedGrammar`. + +3. `orderedGrammar` gives the desired order for the nonterminals and productions +in the documented grammar. Developers should edit this file to change the order. +`doc_grammar` updates `orderedGrammar` so it has the same set of nonterminals and productions +as `editedGrammar`. The update process removes manually-added comments from +`orderedGrammar` while automatically-generated comments will be regenerated. + +4. The tool applies further edits to the grammar specified by `productionlist.edit_mlg`, +then it updates the productionlists in the `.rst` files as specified by comments in the form +`.. insertgram <first nt> <last nt>`. The edits are primarily to expand +`.mlg` constructs such as `LIST1` and `OPT` into separate productions. The tool +generates `productionlistGrammar`, which has the entire grammar in the form of `productionlists`. + +5. Using the grammar produced in step 3, the tool applies edits specified by +`prodn.edit_mlg` and generates `prodnGrammar`, representing each production as +a Sphinx `prodn` construct. Differently-edited grammars are used because `prodn` +can naturally represent `LIST1 x SEP ','` whereas that is awkward for `productionlists`. + +## How to use the tool + +* `make doc_gram` updates `fullGrammar`. + +* `make doc_gram_verify` verifies that `fullGrammar` is consistent with the `.mlg` files. + This is for use by CI. + +* `make doc_gram_rsts` updates the `*Grammar` and `.rst` files. + +Changes to `fullGrammar`, `orderedGrammar` and the `.rsts` should be checked in to git. +The other `*Grammar` files should not. + +### Command line arguments + +The executable takes a list of `.mlg` and `.rst` files as arguments. The tool +inserts the grammar into the `.rsts` as specified by comments in those files. +The order of the `.mlg` files affects the order of nonterminals and productions in +`fullGrammar`. The order doesn't matter for the `.rst` files. + +Specifying the `-verify` command line argument avoids updating any of the files, +but verifies that the current files are consistent. This setting is meant for +use in CI; it will be up to each developer to include the changes to `*Grammar` and +the `.rst` files in their PRs when they've changed the grammar. + +Other command line arguments: + +* `-check-tacs` reports on differences in tactics between the `rsts` and the grammar + +* `-check-cmds` reports on differences in commands between the `rsts` and the grammar + +* `-no-warn` suppresses printing of some warning messages + +* `-short` limits processing to updating/verifying only the `fullGrammar` file + +* `-verbose` prints more messages about the grammar + +* `-verify` described above + +### Grammar editing scripts + +The grammar editing scripts `*.edit_mlg` are similar in format to `.mlg` files stripped +of all OCaml features. This is an easy way to include productions to match or add without +writing another parser. The `DOC_GRAMMAR` token at the beginning of each file +signals the use of streamlined syntax. + +Each edit file has a series of items in the form of productions. Items are applied +in the order they appear. There are two types of editing operations: + +* Global edits - edit rules that apply to the entire grammar in a single operation. + These are identified by using specific reserved names as the non-terminal name. + +* Local edits - edit rules that apply to the productions of a single non-terminal. + The rule is a local edit if the non-terminal name isn't reserved. Individual + productions within a local edit that begin with a different set of reserved names + edit existing productions. For example `binders: [ | DELETE Pcoq.Constr.binders ]` + deletes the production `binders: [ | Pcoq.Constr.binders]` + +Productions that don't begin with a reserved name are added to the grammar, +such as `empty: [ | ]`, which adds a new non-terminal `empty` with an +empty production on the right-hand side. + +Another example: `LEFTQMARK: [ | "?" ]` is a local edit that treats `LEFTQMARK` as +the name of a non-terminal and adds one production for it. (We know that LEFTQMARK +is a token but doc_grammar does not.) `SPLICE: [ | LEFTQMARK ]` requests replacing all +uses of `LEFTQMARK` anywhere in the grammar with its productions and removing the +non-terminal. The combined effect of these two is to replace all uses of +`LEFTQMARK` with `"?"`. + +Here are the current operations. They are likely to be refined as we learn +what operations are most useful while we update the mlg files and documentation: + +### Global edits + +`DELETE` - deletes the specified non-terminals anywhere in the grammar. Each +should appear as a separate production. Useful for removing non-terminals that +only do lookahead that shouldn't be in the documentation. + +`RENAME` - each production specifies an (old name, new name) pair of +non-terminals to rename. + +`SPLICE` - requests replacing all uses of the nonterminals anywhere in the +grammar with its productions and removing the non-terminal. Each should appear +as a separate production. (Doesn't work recursively; splicing for both +`A: [ | B ]` and `B: [ | C ]` must be done in separate SPLICE operations.) + +`EXPAND` - expands LIST0, LIST1, LIST* ... SEP and OPT constructs into +new non-terminals + +### Local edits + +`DELETE <production>` - removes the specified production from the grammar + +`EDIT <production>` - modifies the specified production using the following tags +that appear in the specified production: + +* `USE_NT <name>` LIST* - extracts LIST* as new nonterminal with the specified + new non-terminal name + +* `ADD_OPT <grammar symbol>` - looks for a production that matches the specified + production **without** `<grammar_symbol>`. If found, both productions are + replaced with single production with `OPT <grammar_symbol>` + + The current version handles a single USE_NT or ADD_OPT per EDIT. + +* `REPLACE` - (2 sequential productions) - removes `<oldprod>` and + inserts `<newprod>` in its place. + +``` +| REPLACE <oldprod> +| WITH <newprod> +``` + +* (any other nonterminal name) - adds a new production (and possibly a new nonterminal) +to the grammar. + +### `.rst` file updates + +`doc_grammar` updates `.rst` files when it sees the following 3 lines + +``` +.. insertgram <start> <end> +.. productionlist:: XXX +``` + +The end of the existing `productionlist` is recognized by a blank line. + +### Other details + +The output identifies productions from plugins that aren't automatically loaded with +`(* XXX plugin *)` in grammar files and with `(XXX plugin)` in productionlists. +If desired, this mechanism could be extended to tag certain productions as deprecated, +perhaps in conjunction with a coqpp change. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg new file mode 100644 index 0000000000..ea94e21ff3 --- /dev/null +++ b/doc/tools/docgram/common.edit_mlg @@ -0,0 +1,220 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Defines additional productions and edits for use in documentation. Not compiled into Coq *) + +DOC_GRAMMAR + +(* additional nts to be spliced *) + +LEFTQMARK: [ +| "?" +] + +SPLICE: [ +| LEFTQMARK +] + +hyp: [ +| var +] + +tactic_then_gen: [ +| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen +| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last +] + +SPLICE: [ +| hyp +| identref +| pattern_ident (* depends on previous LEFTQMARK splice todo: improve *) +| constr_eval (* splices as multiple prods *) +| tactic_then_last (* todo: dependency on c.edit_mlg edit?? really useful? *) +| Prim.name +| ltac_selector +| Constr.ident +| tactic_then_locality (* todo: cleanup *) +| attribute_list +] + +RENAME: [ + (* map missing names for rhs *) +| _binders binders +| Constr.constr term +| Constr.constr_pattern constr_pattern +| Constr.global global +| Constr.lconstr lconstr +| Constr.lconstr_pattern lconstr_pattern +| G_vernac.query_command query_command +| G_vernac.section_subset_expr section_subset_expr +| nonsimple_intropattern intropattern +| Pltac.tactic tactic +| Pltac.tactic_expr ltac_expr +| Prim.ident ident +| Prim.reference reference +| Pvernac.Vernac_.main_entry vernac_control +| Tactic.tactic tactic +| tactic3 ltac_expr3 (* todo: can't figure out how this gets mapped by coqpp *) +| tactic1 ltac_expr1 (* todo: can't figure out how this gets mapped by coqpp *) +| tactic0 ltac_expr0 (* todo: can't figure out how this gets mapped by coqpp *) +| tactic_expr5 ltac_expr +| tactic_expr4 ltac_expr4 +| tactic_expr3 ltac_expr3 +| tactic_expr2 ltac_expr2 +| tactic_expr1 ltac_expr1 +| tactic_expr0 ltac_expr0 + + (* elementary renaming/OCaml-defined productions *) +| clause clause_dft_concl +| in_clause' in_clause +| l_constr lconstr (* todo: should delete the production *) + + (* SSR *) +| G_vernac.def_body def_body +| Pcoq.Constr.constr term +| Prim.by_notation by_notation +| Prim.identref ident +| Prim.natural natural +| Vernac.rec_definition rec_definition + + (* rename on lhs *) +| intropatterns intropattern_list_opt +| Constr.closed_binder closed_binder + + (* historical name *) +| constr term +] + +DELETE: [ +| check_for_coloneq +| impl_ident_head +| local_test_lpar_id_colon +| lookup_at_as_comma +| only_starredidentrefs +| test_bracket_ident +| test_lpar_id_coloneq +| test_lpar_id_rpar +| test_lpar_idnum_coloneq +| test_show_goal + + (* SSR *) +(* | ssr_null_entry *) +| ssrtermkind (* todo: rename as "test..." *) +| term_annotation (* todo: rename as "test..." *) +| test_idcomma +| test_nohidden +| test_not_ssrslashnum +| test_ssr_rw_syntax +| test_ssreqid +| test_ssrfwdid +| test_ssrseqvar +| test_ssrslashnum00 +| test_ssrslashnum01 +| test_ssrslashnum10 +| test_ssrslashnum11 +| test_ident_no_do +| ssrdoarg (* todo: this and the next one should be removed from the grammar? *) +| ssrseqdir +] + +ident: [ +| DELETE IDENT ssr_null_entry +] + +natural: [ +| DELETE _natural +] + + + (* added productions *) + +empty: [ (* todo: (bug) this is getting converted to empty -> empty *) +| +] + +lpar_id_coloneq: [ +| "(" IDENT; ":=" +] + +name_colon: [ +| IDENT; ":" +| "_" ":" (* todo: should "_" be a keyword or an identifier? *) +] + +int: [ (* todo: probably should be NUMERAL *) +| integer +] + +command_entry: [ +| noedit_mode +] + +binders: [ +| DELETE Pcoq.Constr.binders (* todo: not sure why there are 2 "binders:" *) +] + +(* edits to simplify *) + +ltac_expr1: [ +| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end" +] + +match_context_list: [ +| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|" +] + +match_hyps: [ +| REPLACE name ":=" "[" match_pattern "]" ":" match_pattern +| WITH name ":=" OPT ("[" match_pattern "]" ":") match_pattern +| DELETE name ":=" match_pattern +] + +match_list: [ +| EDIT ADD_OPT "|" LIST1 match_rule SEP "|" +] + + +selector_body: [ +| REPLACE range_selector_or_nth (* depends on whether range_selector_or_nth is deleted first *) +| WITH LIST1 range_selector SEP "," +] + +range_selector_or_nth: [ +| DELETENT +] + +simple_tactic: [ +| DELETE "intros" +| REPLACE "intros" ne_intropatterns +| WITH "intros" intropattern_list_opt +| DELETE "eintros" +| REPLACE "eintros" ne_intropatterns +| WITH "eintros" intropattern_list_opt +] + +intropattern_list_opt: [ +| DELETE LIST0 intropattern +| intropattern_list_opt intropattern +| empty +] + + +ne_intropatterns: [ +| DELETENT (* todo: don't use DELETENT for this *) +] + + +or_and_intropattern: [ +| DELETE "()" +| DELETE "(" simple_intropattern ")" +| REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")" +| WITH "(" LIST0 simple_intropattern SEP "," ")" +| EDIT "[" USE_NT intropattern_or LIST1 intropattern_list_opt SEP "|" "]" +] diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml new file mode 100644 index 0000000000..eb86bab37e --- /dev/null +++ b/doc/tools/docgram/doc_grammar.ml @@ -0,0 +1,1606 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Coqpp_parser +open Coqpp_ast + +let exit_code = ref 0 +let show_warn = ref true + +let fprintf = Printf.fprintf + +let error s = + exit_code := 1; + Printf.eprintf "Error: "; + Printf.eprintf s + +(* todo: checking if !show_warn is true here gives a compilation error *) +let warn s = + Printf.eprintf "Warning: "; + Printf.eprintf s + +type args = { + mlg_files : string list; + rst_files : string list; + fullGrammar : bool; + check_tacs : bool; + check_cmds : bool; + show_warn : bool; + verbose : bool; + verify : bool; +} + +let default_args = { + mlg_files = []; + rst_files = []; + fullGrammar = false; + check_tacs = false; + check_cmds = false; + show_warn = true; + verbose = false; + verify = false; +} + +(* translated symbols *) + +type doc_symbol = +| Sterm of string +| Snterm of string +| Slist1 of doc_symbol +| Slist1sep of doc_symbol * doc_symbol +| Slist0 of doc_symbol +| Slist0sep of doc_symbol * doc_symbol +| Sopt of doc_symbol +| Sparen of doc_symbol list (* for GRAMMAR EXTEND *) +| Sprod of doc_symbol list list (* for GRAMMAR EXTEND *) + (* editing operations *) +| Sedit of string +| Sedit2 of string * string + +(* nonterminals to rename or delete *) +module StringMap = Map.Make(String) +module NTMap = StringMap +module StringSet = Set.Make(String) + +type gram = { + (* map from nonterminal name to a list of prods *) + (* each production is a list of doc_symbol *) + map: doc_symbol list list NTMap.t; + (* specifies the order for nt's *) + order: string list; +} + +module DocGram = struct + (* these guarantee that order and map have a 1-1 relationship + on the nt name. They don't guarantee that nts on rhs of a production + are defined, nor do they prohibit duplicate productions *) + + exception Duplicate + exception Invalid + + (* add an nt at the end (if not already present) then set its prods *) + let g_maybe_add g nt prods = + if not (NTMap.mem nt !g.map) then + g := { !g with order = !g.order @ [nt] }; + g := { !g with map = NTMap.add nt prods !g.map } + + (* add an nt at the beginning (if not already present) then set its prods *) + let g_maybe_add_begin g nt prods = + if not (NTMap.mem nt !g.map) then + g := { !g with order = nt :: !g.order }; + g := { !g with map = NTMap.add nt prods !g.map } + + (* reverse the order of the grammar *) + let g_reverse g = + g := { !g with order = List.rev !g.order } + + (* update the productions of an existing nt *) + let g_update_prods g nt prods = + ignore (NTMap.find nt !g.map); (* don't add the nt if it's not present *) + g := { !g with map = NTMap.add nt prods !g.map } + + (* remove a non-terminal *) + let g_remove g nt = + g := { map = NTMap.remove nt !g.map; + order = List.filter (fun elt -> elt <> nt) !g.order } + + (* rename an nt and update its prods, keeping its original position. + If the new name already exists, include its prods *) + let g_rename_merge g nt nt' nprods = + let oprods = + try + let oprods = NTMap.find nt' !g.map in + g := { !g with order = List.filter (fun elt -> elt <> nt') !g.order }; + oprods + with Not_found -> + g := { !g with map = NTMap.add nt' [] !g.map }; + [] + in + g := { map = NTMap.remove nt !g.map; + order = List.map (fun n -> if n = nt then nt' else n) !g.order }; + g_update_prods g nt' (oprods @ nprods) + + (* add a new nonterminal after "ins_after" None means insert at the beginning *) + let g_add_after g ins_after nt prods = + if NTMap.mem nt !g.map then raise Duplicate; (* don't update the nt if it's already present *) + let rec insert_nt order res = + match ins_after, order with + | None, _ -> nt :: order + | Some _, [] -> raise Not_found + | Some ins_after_nt, hd :: tl -> + if hd = ins_after_nt then + (List.rev res) @ (hd :: nt :: tl) + else + insert_nt tl (hd :: res) + in + g := { order = insert_nt !g.order []; + map = NTMap.add nt prods !g.map } + + (* replace the map and order *) + let g_reorder g map order = + let order_nts = StringSet.of_list order in + let map_nts = List.fold_left (fun res b -> let (nt, _) = b in StringSet.add nt res) + StringSet.empty (NTMap.bindings map) in + if List.length order <> NTMap.cardinal map || + not (StringSet.equal order_nts map_nts) then raise Invalid; + g := { order = order; map = map } + +end +open DocGram + +(*** Print routines ***) + +let sprintf = Printf.sprintf + +let map_and_concat f ?(delim="") l = + String.concat delim (List.map f l) + +let rec db_output_prodn = function + | Sterm s -> sprintf "(Sterm %s) " s + | Snterm s -> sprintf "(Snterm %s) " s + | Slist1 sym -> sprintf "(Slist1 %s) " (db_output_prodn sym) + | Slist1sep (sym, sep) -> sprintf "(Slist1sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) + | Slist0 sym -> sprintf "(Slist0 %s) " (db_output_prodn sym) + | Slist0sep (sym, sep) -> sprintf "(Slist0sep %s %s) " (db_output_prodn sep) (db_output_prodn sym) + | Sopt sym -> sprintf "(Sopt %s) " (db_output_prodn sym) + | Sparen prod -> sprintf "(Sparen %s) " (db_out_list prod) + | Sprod prods -> sprintf "(Sprod %s) " (db_out_prods prods) + | Sedit s -> sprintf "(Sedit %s) " s + | Sedit2 (s, s2) -> sprintf "(Sedit2 %s %s) " s s2 +and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod) +and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods) + +let rec output_prod plist need_semi = function + | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s + | Snterm s -> + if plist then sprintf "`%s`" s else + sprintf "%s%s" s (if s = "IDENT" && need_semi then ";" else "") + | Slist1 sym -> sprintf "LIST1 %s" (prod_to_str ~plist [sym]) + | Slist1sep (sym, sep) -> sprintf "LIST1 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) + | Slist0 sym -> sprintf "LIST0 %s" (prod_to_str ~plist [sym]) + | Slist0sep (sym, sep) -> sprintf "LIST0 %s SEP %s" (prod_to_str ~plist [sym]) (prod_to_str ~plist [sep]) + | Sopt sym -> sprintf "OPT %s" (prod_to_str ~plist [sym]) + | Sparen sym_list -> sprintf "( %s )" (prod_to_str sym_list) + | Sprod sym_list -> + sprintf "[ %s ]" (String.concat " " (List.mapi (fun i r -> + let prod = (prod_to_str r) in + let sep = if i = 0 then "" else + if prod <> "" then "| " else "|" in + sprintf "%s%s" sep prod) + sym_list)) + | Sedit s -> sprintf "%s" s + (* todo: make PLUGIN info output conditional on the set of prods? *) + | Sedit2 ("PLUGIN", plugin) -> + if plist then + sprintf " (%s plugin)" plugin + else + sprintf " (* %s plugin *)" plugin + | Sedit2 ("FILE", file) -> + let file_suffix_regex = Str.regexp ".*/\\([a-zA-Z0-9_\\.]+\\)" in + let suffix = if Str.string_match file_suffix_regex file 0 then Str.matched_group 1 file else file in + if plist then + sprintf " (%s)" suffix + else + sprintf " (* %s *)" suffix + | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 + +and prod_to_str_r plist prod = + match prod with + | p :: tl -> + let need_semi = + match prod with + | Snterm "IDENT" :: Sterm _ :: _ + | Snterm "IDENT" :: Sprod _ :: _ -> true + | _ -> false in + (output_prod plist need_semi p) :: (prod_to_str_r plist tl) + | [] -> [] + +and prod_to_str ?(plist=false) prod = + String.concat " " (prod_to_str_r plist prod) + + +let rec output_prodn = function + | Sterm s -> let s = if List.mem s ["{"; "{|"; "|"; "}"] then "%" ^ s else s in + sprintf "%s" s + | Snterm s -> sprintf "@%s" s + | Slist1 sym -> sprintf "{+ %s }" (output_prodn sym) + | Slist1sep (sym, sep) -> sprintf "{+%s %s }" (output_sep sep) (output_prodn sym) + | Slist0 sym -> sprintf "{* %s }" (output_prodn sym) + | Slist0sep (sym, sep) -> sprintf "{*%s %s }" (output_sep sep) (output_prodn sym) + | Sopt sym -> sprintf "{? %s }" (output_prodn sym) + | Sparen sym_list -> sprintf "%s" (prod_to_prodn sym_list) + | Sprod sym_list -> + let lcurly, rcurly = if List.length sym_list = 1 then "", "" else "{| ", " }" in + sprintf "%s%s%s" + lcurly + (String.concat " " (List.mapi (fun i r -> + let prod = (prod_to_prodn r) in + let sep = if i = 0 then "" else + if prod <> "" then "| " else "|" in + sprintf "%s%s" sep prod) + sym_list)) + rcurly + | Sedit s -> sprintf "%s" s + | Sedit2 ("PLUGIN", s2) -> "" + | Sedit2 (s, s2) -> sprintf "%s \"%s\"" s s2 + +and output_sep sep = + match sep with + | Sterm s -> sprintf "%s" s (* avoid escaping separator *) + | _ -> output_prodn sep + +and prod_to_prodn prod = String.concat " " (List.map output_prodn prod) + +type fmt = [`MLG | `PRODLIST | `PRODN ] + +(* print a subset of the grammar with nts in the specified order *) +let print_in_order out g fmt nt_order hide = + List.iter (fun nt -> + if not (StringSet.mem nt hide) then + try + let prods = NTMap.find nt !g.map in + match fmt with + | `MLG -> + fprintf out "%s: [\n" nt; + List.iter (fun prod -> + let str = prod_to_str ~plist:false prod in + let pfx = if str = "" then "|" else "| " in + fprintf out "%s%s\n" pfx str) + prods; + fprintf out "]\n\n" + | `PRODLIST -> + fprintf out "%s :" nt; + List.iteri (fun i prod -> + if i > 0 then + fprintf out "%s :" (String.make (String.length nt) ' '); + let str = prod_to_str ~plist:true prod in + let pfx = if str = "" then "" else " " in + fprintf out "%s%s\n" pfx str) + prods; + | `PRODN -> + fprintf out "\n%s:\n" nt; + List.iter (fun prod -> + let str = prod_to_prodn prod in + let pfx = if str = "" then "" else " " in + fprintf out "%s%s\n" pfx str) + prods; + with Not_found -> error "Missing nt '%s' in print_in_order\n" nt) + nt_order + + +(*** Read grammar routines ***) + +let cvt_ext prod = + let rec to_doc_sym = function + | Ulist1 sym -> Slist1 (to_doc_sym sym) + | Ulist1sep (sym, s) -> Slist1sep ((to_doc_sym sym), Sterm s) + | Ulist0 sym -> Slist0 (to_doc_sym sym) + | Ulist0sep (sym, s) -> Slist0sep ((to_doc_sym sym), Sterm s) + | Uopt sym -> Sopt (to_doc_sym sym) + | Uentry s -> Snterm s + | Uentryl (s, i) -> Snterm (s ^ (string_of_int i)) + in + let from_ext = function + | ExtTerminal s -> Sterm s + | ExtNonTerminal (s, _) -> to_doc_sym s + in + List.map from_ext prod + +let rec cvt_gram_sym = function + | GSymbString s -> Sterm s + | GSymbQualid (s, level) -> + Snterm (match level with + | Some str -> s ^ str + | None -> s) + | GSymbParen l -> Sparen (cvt_gram_sym_list l) + | GSymbProd ll -> + let cvt = List.map cvt_gram_prod ll in + (match cvt with + | (Snterm x :: []) :: [] -> Snterm x + | (Sterm x :: []) :: [] -> Sterm x + | _ -> Sprod cvt) + +and cvt_gram_sym_list l = + let get_sym = function + | GSymbQualid (s, level) -> s + | _ -> "" + in + + match l with + | GSymbQualid ("LIST0", _) :: s :: GSymbQualid ("SEP", _) :: sep :: tl -> + Slist0sep (cvt_gram_sym s, cvt_gram_sym sep) :: cvt_gram_sym_list tl + | GSymbQualid ("LIST1", _) :: s :: GSymbQualid ("SEP", _) :: sep :: tl -> + Slist1sep (cvt_gram_sym s, cvt_gram_sym sep) :: cvt_gram_sym_list tl + | GSymbQualid ("LIST0", _) :: s :: tl -> + Slist0 (cvt_gram_sym s) :: cvt_gram_sym_list tl + | GSymbQualid ("LIST1", _) :: s :: tl -> + Slist1 (cvt_gram_sym s) :: cvt_gram_sym_list tl + | GSymbQualid ("OPT", _) :: s :: tl -> + Sopt (cvt_gram_sym s) :: cvt_gram_sym_list tl + | GSymbQualid ("IDENT", _) :: s2 :: tl when get_sym s2 = "" -> + cvt_gram_sym s2 :: cvt_gram_sym_list tl + | GSymbQualid ("ADD_OPT", _) :: tl -> + (Sedit "ADD_OPT") :: cvt_gram_sym_list tl + | GSymbQualid ("NOTE", _) :: GSymbQualid (s2, l) :: tl -> + (Sedit2 ("NOTE", s2)) :: cvt_gram_sym_list tl + | GSymbQualid ("USE_NT", _) :: GSymbQualid (s2, l) :: tl -> + (Sedit2 ("USE_NT", s2)) :: cvt_gram_sym_list tl + | hd :: tl -> + cvt_gram_sym hd :: cvt_gram_sym_list tl + | [] -> [] + +and cvt_gram_prod p = + List.concat (List.map (fun x -> let _, gs = x in cvt_gram_sym_list gs) p.gprod_symbs) + + +let add_symdef nt file symdef_map = + let ent = + try + StringMap.find nt !symdef_map + with Not_found -> [] + in + symdef_map := StringMap.add nt (Filename.basename file::ent) !symdef_map + +let rec edit_SELF nt cur_level next_level right_assoc prod = + let len = List.length prod in + List.mapi (fun i sym -> + match sym with + | Snterm s -> begin match s with + | s when s = nt || s = "SELF" -> + if i = 0 then Snterm next_level + else if i+1 < len then sym + else if right_assoc then Snterm cur_level else Snterm next_level + | "NEXT" -> Snterm next_level + | _ -> sym + end + | Slist1 sym -> Slist1 (List.hd (edit_SELF nt cur_level next_level right_assoc [sym])) + | Slist0 sym -> Slist0 (List.hd (edit_SELF nt cur_level next_level right_assoc [sym])) + | x -> x) + prod + + +let autoloaded_mlgs = [ (* in the order they are loaded by Coq *) + "parsing/g_constr.mlg"; + "parsing/g_prim.mlg"; + "vernac/g_vernac.mlg"; + "vernac/g_proofs.mlg"; + "toplevel/g_toplevel.mlg"; + "plugins/ltac/extraargs.mlg"; + "plugins/ltac/g_obligations.mlg"; + "plugins/ltac/coretactics.mlg"; + "plugins/ltac/extratactics.mlg"; + "plugins/ltac/profile_ltac_tactics.mlg"; + "plugins/ltac/g_auto.mlg"; + "plugins/ltac/g_class.mlg"; + "plugins/ltac/g_rewrite.mlg"; + "plugins/ltac/g_eqdecide.mlg"; + "plugins/ltac/g_tactic.mlg"; + "plugins/ltac/g_ltac.mlg"; + "plugins/syntax/g_string.mlg"; + "plugins/btauto/g_btauto.mlg"; + "plugins/rtauto/g_rtauto.mlg"; + "plugins/cc/g_congruence.mlg"; + "plugins/firstorder/g_ground.mlg"; + "plugins/syntax/g_numeral.mlg"; +] + + +let ematch prod edit = + let rec ematchr prod edit = + (*Printf.printf "%s and\n %s\n\n" (prod_to_str prod) (prod_to_str edit);*) + match (prod, edit) with + | (_, Sedit _ :: tl) + | (_, Sedit2 _ :: tl) + -> ematchr prod tl + | (Sedit _ :: tl, _) + | (Sedit2 _ :: tl, _) + -> ematchr tl edit + | (phd :: ptl, hd :: tl) -> + let m = match (phd, hd) with + | (Slist1 psym, Slist1 sym) + | (Slist0 psym, Slist0 sym) + | (Sopt psym, Sopt sym) + -> ematchr [psym] [sym] + | (Slist1sep (psym, psep), Slist1sep (sym, sep)) + | (Slist0sep (psym, psep), Slist0sep (sym, sep)) + -> ematchr [psym] [sym] && ematchr [psep] [sep] + | (Sparen psyml, Sparen syml) + -> ematchr psyml syml + | (Sprod psymll, Sprod symll) + -> List.fold_left (&&) true (List.map2 ematchr psymll symll) + | _, _ -> phd = hd + in + m && ematchr ptl tl + | ([], hd :: tl) -> false + | (phd :: ptl, []) -> false + | ([], []) -> true +in + (*Printf.printf "\n";*) + let rv = ematchr prod edit in + (*Printf.printf "%b\n" rv;*) + rv + +let has_match p prods = List.exists (fun p2 -> ematch p p2) prods + +let plugin_regex = Str.regexp "^plugins/\\([a-zA-Z0-9_]+\\)/" + +let read_mlg is_edit ast file level_renames symdef_map = + let res = ref [] in + let add_prods nt prods = + if not is_edit then + add_symdef nt file symdef_map; + let prods = if not is_edit && + not (List.mem file autoloaded_mlgs) && + Str.string_match plugin_regex file 0 then + let plugin = Str.matched_group 1 file in + List.map (fun p -> p @ [Sedit2 ("PLUGIN", plugin)]) prods + else + prods + in + (* todo: doesn't yet work perfectly with SPLICE *) +(* let prods = if not is_edit then List.map (fun p -> p @ [Sedit2 ("FILE", file)]) prods else prods in*) + res := (nt, prods) :: !res + in + let prod_loop = function + | GramExt grammar_ext -> + let get_label = function + | Some s -> s + | None -> "" + in + List.iter (fun ent -> + let len = List.length ent.gentry_rules in + List.iteri (fun i rule -> + let nt = ent.gentry_name in + let level = (get_label rule.grule_label) in + let level = if level <> "" then level else + match ent.gentry_pos with + | Some Level lev + | Some Before lev + | Some After lev + -> lev + (* Looks like FIRST/LAST can be ignored for documenting the current grammar *) + | _ -> "" in + let cur_level = nt ^ level in + let next_level = nt ^ + if i+1 < len then (get_label (List.nth ent.gentry_rules (i+1)).grule_label) else "" in + let right_assoc = (rule.grule_assoc = Some RightA) in + + if i = 0 && cur_level <> nt && not (StringMap.mem nt !level_renames) then begin + level_renames := StringMap.add nt cur_level !level_renames; + end; + let cvted = List.map cvt_gram_prod rule.grule_prods in + (* edit names for levels *) + (* See https://camlp5.github.io/doc/html/grammars.html#b:Associativity *) + let edited = List.map (edit_SELF nt cur_level next_level right_assoc) cvted in + let prods_to_add = + if cur_level <> nt && i+1 < len then + edited @ [[Snterm next_level]] + else + edited in + add_prods cur_level prods_to_add) + ent.gentry_rules + ) grammar_ext.gramext_entries + + | VernacExt vernac_ext -> + let node = match vernac_ext.vernacext_entry with + | None -> "command" + | Some c -> String.trim c.code + in + add_prods node + (List.map (fun r -> cvt_ext r.vernac_toks) vernac_ext.vernacext_rules) + | VernacArgumentExt vernac_argument_ext -> + add_prods vernac_argument_ext.vernacargext_name + (List.map (fun r -> cvt_ext r.tac_toks) vernac_argument_ext.vernacargext_rules) + | TacticExt tactic_ext -> + add_prods "simple_tactic" + (List.map (fun r -> cvt_ext r.tac_toks) tactic_ext.tacext_rules) + | ArgumentExt argument_ext -> + add_prods argument_ext.argext_name + (List.map (fun r -> cvt_ext r.tac_toks) argument_ext.argext_rules) + | _ -> () + in + + List.iter prod_loop ast; + List.rev !res + +let dir s = "doc/tools/docgram/" ^ s + +let read_mlg_edit file = + let fdir = dir file in + let level_renames = ref StringMap.empty in (* ignored *) + let symdef_map = ref StringMap.empty in (* ignored *) + read_mlg true (parse_file fdir) fdir level_renames symdef_map + +let add_rule g nt prods file = + let ent = try NTMap.find nt !g.map with Not_found -> [] in + let nodups = List.concat (List.map (fun prod -> + if has_match prod ent then begin + if !show_warn then + warn "%s: Duplicate production '%s: %s'\n" file nt (prod_to_str prod); + [] + end else + [prod]) + prods) in + g_maybe_add_begin g nt (ent @ nodups) + +let read_mlg_files g args symdef_map = + let level_renames = ref StringMap.empty in + let last_autoloaded = List.hd (List.rev autoloaded_mlgs) in + List.iter (fun file -> + (* does nt renaming, deletion and splicing *) + let rules = read_mlg false (parse_file file) file level_renames symdef_map in + let numprods = List.fold_left (fun num rule -> + let nt, prods = rule in + add_rule g nt prods file; + num + List.length prods) + 0 rules + in + if args.verbose then begin + Printf.eprintf "%s: %d nts, %d prods\n" file (List.length rules) numprods; + if file = last_autoloaded then + Printf.eprintf " Optionally loaded plugins:\n" + end + ) args.mlg_files; + g_reverse g; + !level_renames + + +(*** global editing ops ***) + +let create_edit_map edits = + let rec aux edits map = + match edits with + | [] -> map + | edit :: tl -> + let (key, binding) = edit in + aux tl (StringMap.add key binding map) + in + aux edits StringMap.empty + +(* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *) +let rec edit_prod g top edit_map prod = + let edit_nt edit_map sym0 nt = + try + let binding = StringMap.find nt edit_map in + match binding with + | "DELETE" -> [] + | "SPLICE" -> + begin + try let splice_prods = NTMap.find nt !g.map in + match splice_prods with + | [] -> assert false + | [p] -> List.rev p + | _ -> [Sprod splice_prods] + with Not_found -> error "Missing nt '%s' for splice\n" nt; [Snterm nt] + end + | _ -> [Snterm binding] + with Not_found -> [sym0] + in + + let rec edit_symbol sym0 = + match sym0 with + | Sterm s -> [sym0] + | Snterm s -> edit_nt edit_map sym0 s + | Slist1 sym -> [Slist1 (List.hd (edit_symbol sym))] + (* you'll get a run-time failure deleting a SEP symbol *) + | Slist1sep (sym, sep) -> [Slist1sep (List.hd (edit_symbol sym), (List.hd (edit_symbol sep)))] + | Slist0 sym -> [Slist0 (List.hd (edit_symbol sym))] + | Slist0sep (sym, sep) -> [Slist0sep (List.hd (edit_symbol sym), (List.hd (edit_symbol sep)))] + | Sopt sym -> [Sopt (List.hd (edit_symbol sym))] + | Sparen slist -> [Sparen (List.hd (edit_prod g false edit_map slist))] + | Sprod slistlist -> let (_, prods) = edit_rule g edit_map "" slistlist in + [Sprod prods] + | Sedit _ + | Sedit2 _ -> [sym0] (* these constructors not used here *) + in + let is_splice nt = + try + StringMap.find nt edit_map = "SPLICE" + with Not_found -> false + in + let get_splice_prods nt = + try NTMap.find nt !g.map + with Not_found -> (error "Missing nt '%s' for splice\n" nt; []) + in + + (* special case splice creating multiple new productions *) + let splice_prods = match prod with + | Snterm nt :: [] when is_splice nt -> + get_splice_prods nt + | _ -> [] + in + if top && splice_prods <> [] then + splice_prods + else + [List.rev (List.concat (List.rev (List.map (fun sym -> edit_symbol sym) prod)))] + +and edit_rule g edit_map nt rule = + let nt = + try let new_name = StringMap.find nt edit_map in + match new_name with + | "SPLICE" -> nt + | "DELETE" -> "" + | _ -> new_name + with Not_found -> nt + in + (nt, (List.concat (List.map (edit_prod g true edit_map) rule))) + +(*** splice: replace a reference to a nonterminal with its definition ***) + +(* todo: create a better splice routine, handle recursive case *) +let apply_splice g splice_map = + StringMap.iter (fun nt b -> + if not (NTMap.mem nt !g.map) then + error "Unknown nt '%s' for apply_splice\n" nt) + splice_map; + List.iter (fun b -> + let (nt, prods) = b in + let (nt', prods) = edit_rule g splice_map nt prods in + g_update_prods g nt' prods) + (NTMap.bindings !g.map); + List.iter (fun b -> + let (nt, op) = b in + match op with + | "DELETE" + | "SPLICE" -> + g_remove g nt; + | _ -> ()) + (StringMap.bindings splice_map) + +let find_first edit prods nt = + let rec find_first_r edit prods nt i = + match prods with + | [] -> + error "Can't find '%s' in REPLACE for '%s'\n" (prod_to_str edit) nt; + raise Not_found + | prod :: tl -> + if ematch prod edit then i + else find_first_r edit tl nt (i+1) + in + find_first_r edit prods nt 0 + +let remove_prod edit prods nt = + let res, got_first = List.fold_left (fun args prod -> + let res, got_first = args in + if not got_first && ematch prod edit then + res, true + else + prod :: res, got_first) + ([], false) prods in + if not got_first then + error "Can't find '%s' to DELETE for '%s'\n" (prod_to_str edit) nt; + List.rev res + +let insert_after posn insert prods = + List.concat (List.mapi (fun i prod -> + if i = posn then prod :: insert else [prod]) + prods) + +(*** replace LIST*, OPT with new nonterminals ***) + +(* generate a non-terminal name for a replacement *) +let nt_regex = Str.regexp "^[a-zA-Z_][a-zA-Z0-9_\\.]*$" +let good_name name = if Str.string_match nt_regex name 0 then name else "" +let map_name s = + let s = match s with + | "|" -> "or" + | "!" -> "exclam" + | ">" -> "gt" + | "<" -> "lt" + | "+" -> "plus" + | "?" -> "qmark" + | "}" -> "rbrace" + | "," -> "comma" + | ";" -> "semi" + | _ -> s + in + good_name s + +let rec gen_nt_name sym = + let name_from_prod prod = + let rec aux name sterm_name prod = + if name <> "" then name else + match prod with + | [] -> sterm_name + | Sterm s :: tl + | Snterm s :: tl -> + if good_name s <> "" then + aux (map_name s) sterm_name tl + else + aux name (map_name s) tl; + | sym :: tl-> + aux (gen_nt_name sym) sterm_name tl + in + aux "" "" prod + in + + let name = match sym with + | Sterm s -> map_name s + | Snterm s -> s + | Slist1 sym + | Slist1sep (sym, _) + | Slist0 sym + | Slist0sep (sym, _) + | Sopt sym -> + gen_nt_name sym + | Sparen slist -> + name_from_prod slist + | Sprod slistlist -> + name_from_prod (List.hd slistlist) + | _ -> "" + in + good_name name + +(* create a new nt for LIST* or OPT with the specified name *) +let rec maybe_add_nt g insert_after name sym queue = + let empty = [Snterm "empty"] in + let maybe_unwrap ?(multi=false) sym = + match sym with + | Sprod slist when List.length slist = 1 || multi + -> slist + | Sparen slist -> [ slist ] + | _ -> [ [sym] ] + in + let unw sym = List.hd (maybe_unwrap sym) in + let get_prods nt = + match sym with + | Slist1 sym -> let sym' = unw sym in + [ [Snterm nt] @ sym'; sym' ] + | Slist1sep (sym, sep) + | Slist0sep (sym, sep) -> let sym' = unw sym in + [ [Snterm nt; sep] @ sym'; sym' ] + | Slist0 sym -> [ [Snterm nt] @ (unw sym); empty ] + | Sopt sym -> (maybe_unwrap ~multi:true sym) @ [ empty ] + | Sprod slistlist -> slistlist + | _ -> [] + in + + let is_slist0sep sym = + match sym with + | Slist0sep _ -> true + | _ -> false + in + + (* find an existing nt with an identical definition, or generate an unused nt name *) + let rec find_name nt i = + let trial_name = sprintf "%s%s" nt (if i = 1 then "" else string_of_int i) in + try + if NTMap.find trial_name !g.map = get_prods trial_name then + trial_name + else + find_name nt (succ i) + with Not_found -> trial_name + in + let list_name sep = + match sep with + | Sterm s -> + let name = map_name s in + if name = s then "_list" else "_list_" ^ name + | _ -> "_list" + in + let nt = name ^ match sym with + | Slist1 sym -> "_list" + | Slist1sep (sym, sep) -> list_name sep + | Slist0 sym -> "_list_opt" + | Slist0sep (sym, sep) -> list_name sep (* special handling *) + | Sopt sym -> "_opt" + | Sprod slistlist -> "_alt" + | _ -> (error "Invalid symbol for USE_NT for nt '%s'\n" name; "ERROR") + in + let base_nt = find_name nt 1 in + let new_nt = if is_slist0sep sym then base_nt ^ "_opt" else base_nt in + if not (NTMap.mem new_nt !g.map) then begin + let prods = if is_slist0sep sym then [ [Snterm base_nt]; empty ] else get_prods base_nt in + g_add_after g (Some !insert_after) new_nt prods; + insert_after := new_nt; + Queue.add new_nt queue + end; + if is_slist0sep sym && not (NTMap.mem base_nt !g.map) then begin + match sym with + | Slist0sep (sym, sep) -> + let prods = get_prods base_nt in + g_add_after g (Some !insert_after) base_nt prods; + insert_after := base_nt; + Queue.add base_nt queue + | _ -> () + end; + new_nt + +(* expand LIST*, OPT and add "empty" *) +(* todo: doesn't handle recursive expansions well, such as syntax_modifier_opt *) +and expand_rule g edited_nt queue = + let rule = NTMap.find edited_nt !g.map in + let insert_after = ref edited_nt in + let rec expand rule = + let rec aux syms res = + match syms with + | [] -> res + | sym0 :: tl -> + let new_sym = match sym0 with + | Sterm _ + | Snterm _ -> + sym0 + | Slist1 sym + | Slist1sep (sym, _) + | Slist0 sym + | Slist0sep (sym, _) + | Sopt sym -> + let name = gen_nt_name sym in + if name <> "" then begin + let new_nt = maybe_add_nt g insert_after name sym0 queue in + Snterm new_nt + end else sym0 + | Sparen slist -> Sparen (expand slist) + | Sprod slistlist -> + let has_empty = List.length (List.hd (List.rev slistlist)) = 0 in + let name = gen_nt_name sym0 in + if name <> "" then begin + let new_nt = maybe_add_nt g insert_after name + (if has_empty then (Sopt (Sprod (List.rev (List.tl (List.rev slistlist))) )) + else sym0) queue + in + Snterm new_nt + end else + Sprod (List.map expand slistlist) + | Sedit _ + | Sedit2 _ -> + sym0 (* these constructors not used here *) + in + aux tl (new_sym :: res) + in + List.rev (aux rule (if edited_nt <> "empty" && ematch rule [] then [Snterm "empty"] else [])) + in + let rule' = List.map expand rule in + g_update_prods g edited_nt rule' + +let expand_lists g = + (* todo: use Queue.of_seq w OCaml 4.07+ *) + let queue = Queue.create () in + List.iter (fun nt -> Queue.add nt queue) !g.order; + try + while true do + let nt = Queue.pop queue in + expand_rule g nt queue + done + with + | Queue.Empty -> () + +let edit_all_prods g op eprods = + let do_it op eprods num = + let rec aux eprods res = + match eprods with + | [] -> res + | [Snterm old_nt; Snterm new_nt] :: tl when num = 2 -> + aux tl ((old_nt, new_nt) :: res) + | [Snterm old_nt] :: tl when num = 1 -> + aux tl ((old_nt, op) :: res) + | eprod :: tl -> + error "Production '%s: %s' must have only %d nonterminal(s)\n" + op (prod_to_str eprod) num; + aux tl res + in + let map = create_edit_map (aux eprods []) in + if op = "SPLICE" then + apply_splice g map + else (* RENAME/DELETE *) + List.iter (fun b -> let (nt, _) = b in + let prods = try NTMap.find nt !g.map with Not_found -> [] in + let (nt', prods') = edit_rule g map nt prods in + if nt' = "" then + g_remove g nt + else if nt <> nt' then + g_rename_merge g nt nt' prods' + else + g_update_prods g nt prods') + (NTMap.bindings !g.map); + in + match op with + | "RENAME" -> do_it op eprods 2; true + | "DELETE" -> do_it op eprods 1; true + | "SPLICE" -> do_it op eprods 1; true + | "EXPAND" -> + if List.length eprods > 1 || List.length (List.hd eprods) <> 0 then + error "'EXPAND:' expects a single empty production\n"; + expand_lists g; true + | _ -> false + +let edit_single_prod g edit0 prods nt = + let rec edit_single_prod_r edit prods nt seen = + match edit with + | [] -> prods + | Sedit "ADD_OPT" :: sym :: tl -> + let prods' = (try + let pfx = List.rev seen in + let posn = find_first edit0 prods nt in + let prods = insert_after posn [pfx @ (Sopt sym :: tl)] prods in + let prods = remove_prod (pfx @ (sym :: tl)) prods nt in + remove_prod (pfx @ tl) prods nt + with Not_found -> prods) in + edit_single_prod_r tl prods' nt seen + | Sedit "ADD_OPT" :: [] -> error "Bad position for ADD_OPT\n"; prods + | Sedit2 ("USE_NT", name) :: sym :: tl -> + let prods' = (try + let nt = maybe_add_nt g (ref nt) name sym (Queue.create ()) in + let pfx = List.rev seen in + let posn = find_first edit0 prods nt in + let prods = insert_after posn [pfx @ (Snterm nt :: tl)] prods in + remove_prod (pfx @ (sym :: tl)) prods nt + with Not_found -> prods) in + edit_single_prod_r tl prods' nt seen + | Sedit2 ("USE_NT", _) :: [] -> error "Bad position for USE_NT\n"; prods + | sym :: tl -> + edit_single_prod_r tl prods nt (sym :: seen) + in + edit_single_prod_r edit0 prods nt [] + +let apply_edit_file g edits = + List.iter (fun b -> + let (nt, eprod) = b in + if not (edit_all_prods g nt eprod) then begin + let rec aux eprod prods add_nt = + match eprod with + | [] -> prods, add_nt + | (Snterm "DELETE" :: oprod) :: tl -> + aux tl (remove_prod oprod prods nt) add_nt + | (Snterm "DELETENT" :: _) :: tl -> (* note this doesn't remove references *) + g_remove g nt; + aux tl prods false + | (Snterm "EDIT" :: oprod) :: tl -> + aux tl (edit_single_prod g oprod prods nt) add_nt + | (Snterm "REPLACE" :: oprod) :: (Snterm "WITH" :: rprod) :: tl -> + let prods' = (try + let posn = find_first oprod prods nt in + let prods = insert_after posn [rprod] prods in (* insert new prod *) + remove_prod oprod prods nt (* remove orig prod *) + with Not_found -> prods) + in + aux tl prods' add_nt + | (Snterm "REPLACE" :: _ as eprod) :: tl -> + error "Missing WITH after '%s' in '%s'\n" (prod_to_str eprod) nt; + aux tl prods add_nt + | prod :: tl -> + (* add a production *) + if has_match prod prods then + error "Duplicate production '%s' for %s\n" (prod_to_str prod) nt; + aux tl (prods @ [prod]) add_nt + in + let prods, add_nt = + aux eprod (try NTMap.find nt !g.map with Not_found -> []) true in + if add_nt then + g_maybe_add g nt prods + end) + edits + + +(*** main routines ***) + + (* get the nt's in the production, preserving order, don't worry about dups *) + let nts_in_prod prod = + let rec traverse = function + | Sterm s -> [] + | Snterm s -> [s] + | Slist1 sym + | Slist0 sym + | Sopt sym + -> traverse sym + | Slist1sep (sym, sep) + | Slist0sep (sym, sep) + -> traverse sym @ (traverse sep) + | Sparen sym_list -> List.concat (List.map traverse sym_list) + | Sprod sym_list_list -> List.concat (List.map (fun l -> List.concat (List.map traverse l)) sym_list_list) + | Sedit _ + | Sedit2 _ -> [] + in + List.rev (List.concat (List.map traverse prod)) + + (* get the special tokens in the grammar *) +let print_special_tokens g = + let rec traverse set = function + | Sterm s -> + let c = s.[0] in + if (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') then set + else StringSet.add s set + | Snterm s -> set + | Slist1 sym + | Slist0 sym + | Sopt sym + -> traverse set sym + | Slist1sep (sym, sep) + | Slist0sep (sym, sep) + -> traverse (traverse set sym) sep + | Sparen sym_list -> traverse_prod set sym_list + | Sprod sym_list_list -> traverse_prods set sym_list_list + | Sedit _ + | Sedit2 _ -> set + and traverse_prod set prod = List.fold_left traverse set prod + and traverse_prods set prods = List.fold_left traverse_prod set prods + in + let spec_toks = List.fold_left (fun set b -> + let nt, prods = b in + traverse_prods set prods) + StringSet.empty (NTMap.bindings !g.map) + in + Printf.printf "Special tokens:"; + StringSet.iter (fun t -> Printf.printf " %s" t) spec_toks; + Printf.printf "\n\n" + +(* get the transitive closure of a non-terminal excluding "stops" symbols. + Preserve ordering to the extent possible *) +(* todo: at the moment, the code doesn't use the ordering; consider switching to using +sets instead of lists *) +let nt_closure g start stops = + let stop_set = StringSet.of_list stops in + let rec nt_closure_r res todo = + match todo with + | [] -> res + | nt :: tl -> + if List.mem nt res || StringSet.mem nt stop_set then + nt_closure_r res tl + else begin + let more_to_do = + try + let prods = NTMap.find nt !g.map in + tl @ (List.concat (List.map nts_in_prod prods)) + with Not_found -> tl in + nt_closure_r (nt :: res) more_to_do + end + in + List.rev (nt_closure_r [] [start]) + +let header = "--------------------------------------------" +let nt_subset_in_orig_order g nts = + let subset = StringSet.of_list nts in + List.filter (fun nt -> StringSet.mem nt subset) !g.order + +let print_chunk out g seen fmt title starts ends = + fprintf out "\n\n%s:\n%s\n" title header; + List.iter (fun start -> + let nts = (nt_closure g start ends) in + print_in_order out g fmt (nt_subset_in_orig_order g nts) !seen; + seen := StringSet.union !seen (StringSet.of_list nts)) + starts + +let print_chunks g out fmt () = + let seen = ref StringSet.empty in + print_chunk out g seen fmt "lconstr" ["lconstr"] ["binder_constr"; "tactic_expr5"]; + print_chunk out g seen fmt "Gallina syntax of terms" ["binder_constr"] ["tactic_expr5"]; + print_chunk out g seen fmt "Gallina The Vernacular" ["gallina"] ["tactic_expr5"]; + print_chunk out g seen fmt "intropattern_list_opt" ["intropattern_list"; "or_and_intropattern_loc"] ["operconstr"; "tactic_expr5"]; + print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] + ["tactic_expr5"; "tactic_expr3"; "tactic_expr2"; "tactic_expr1"; "tactic_expr0"]; + + (*print_chunk out g seen fmt "Ltac" ["tactic_expr5"] [];*) + print_chunk out g seen fmt "Ltac" ["tactic_expr5"] ["tactic_expr4"]; + print_chunk out g seen fmt "Ltac 4" ["tactic_expr4"] ["tactic_expr3"; "tactic_expr2"]; + print_chunk out g seen fmt "Ltac 3" ["tactic_expr3"] ["tactic_expr2"]; + print_chunk out g seen fmt "Ltac 2" ["tactic_expr2"] ["tactic_expr1"]; + print_chunk out g seen fmt "Ltac 1" ["tactic_expr1"] ["tactic_expr0"]; + print_chunk out g seen fmt "Ltac 0" ["tactic_expr0"] []; + + + print_chunk out g seen fmt "command" ["command"] []; + print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] []; + print_chunk out g seen fmt "vernac_control" ["vernac_control"] [] + + (* + let ssr_tops = ["ssr_dthen"; "ssr_else"; "ssr_mpat"; "ssr_rtype"] in + seen := StringSet.union !seen (StringSet.of_list ssr_tops); + + print_chunk out g seen fmt "ssrindex" ["ssrindex"] []; + print_chunk out g seen fmt "command" ["command"] []; + print_chunk out g seen fmt "binder_constr" ["binder_constr"] []; + (*print_chunk out g seen fmt "closed_binder" ["closed_binder"] [];*) + print_chunk out g seen fmt "gallina_ext" ["gallina_ext"] []; + (*print_chunk out g seen fmt "hloc" ["hloc"] [];*) + (*print_chunk out g seen fmt "hypident" ["hypident"] [];*) + print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] []; + print_chunk out g seen fmt "tactic_expr" ["tactic_expr4"; "tactic_expr1"; "tactic_expr0"] []; + fprintf out "\n\nRemainder:\n"; + print_in_order g (List.filter (fun x -> not (StringSet.mem x !seen)) !g.order) StringSet.empty; + *) + + + (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*) + (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*) + +let start_symbols = ["vernac_toplevel"] +(* don't report tokens as undefined *) +let tokens = [ "bullet"; "field"; "ident"; "int"; "num"; "numeral"; "string" ] + +let report_bad_nts g file = + let rec get_nts refd defd bindings = + match bindings with + | [] -> refd, defd + | (nt, prods) :: tl -> + get_nts (List.fold_left (fun res prod -> + StringSet.union res (StringSet.of_list (nts_in_prod prod))) + refd prods) + (StringSet.add nt defd) tl + in + let all_nts_ref, all_nts_def = + get_nts (StringSet.of_list tokens) (StringSet.of_list tokens) (NTMap.bindings !g.map) in + + let undef = StringSet.diff all_nts_ref all_nts_def in + List.iter (fun nt -> warn "%s: Undefined symbol '%s'\n" file nt) (StringSet.elements undef); + + let reachable = + List.fold_left (fun res sym -> + StringSet.union res (StringSet.of_list (nt_closure g sym []))) + StringSet.empty start_symbols + in + let unreachable = List.filter (fun nt -> not (StringSet.mem nt reachable)) !g.order in + List.iter (fun nt -> warn "%s: Unreachable symbol '%s'\n" file nt) unreachable + + +let report_info g symdef_map = + let num_prods = List.fold_left (fun sum nt -> let prods = NTMap.find nt !g.map in sum + (List.length prods)) + 0 !g.order + in + + Printf.eprintf "\nstart symbols: %s\n" (String.concat " " start_symbols); + Printf.eprintf "%d nonterminals defined, %d productions\n" (NTMap.cardinal !g.map) num_prods; + Printf.eprintf "%d terminals\n" (List.length tokens); + + Printf.eprintf "\nSymbols with multiple definition points in *.mlg:\n"; + let bindings = List.sort (fun a b -> let (ak, _) = a and (bk, _) = b in + String.compare ak bk) (StringMap.bindings symdef_map) in + List.iter (fun b -> + let (k, v) = b in + if List.length v > 1 then begin + Printf.eprintf " %s: " k; + List.iter (fun f -> Printf.eprintf "%s " f) v; + Printf.eprintf "\n" + end) + bindings; + Printf.eprintf "\n" + + + +[@@@ocaml.warning "-32"] +let rec dump prod = + match prod with + | hd :: tl -> let s = (match hd with + | Sterm s -> sprintf "Sterm %s" s + | Snterm s -> sprintf "Snterm \"%s\"" s + | Slist1 sym -> "Slist1" + | Slist0 sym -> "Slist0" + | Sopt sym -> "Sopt" + | Slist1sep _ -> "Slist1sep" + | Slist0sep _ -> "Slist0sep" + | Sparen sym_list -> "Sparen" + | Sprod sym_list_list -> "Sprod" + | Sedit _ -> "Sedit" + | Sedit2 _ -> "Sedit2") in + Printf.printf "%s " s; + dump tl + | [] -> Printf.printf "\n" +[@@@ocaml.warning "+32"] + +let reorder_grammar eg reordered_rules file = + let og = ref { map = NTMap.empty; order = [] } in + List.iter (fun rule -> + let nt, prods = rule in + try + (* only keep nts and prods in common with editedGrammar *) + let eg_prods = NTMap.find nt !eg.map in + let prods = List.filter (fun prod -> (has_match prod eg_prods)) prods in + if NTMap.mem nt !og.map then + warn "%s: Duplicate nonterminal '%s'\n" file nt; + add_rule og nt prods file + with Not_found -> ()) + reordered_rules; + g_reverse og; + + (* insert a prod in a list after prev_prod (None=at the beginning) *) + let rec insert_prod prev_prod prod prods res = + match prev_prod, prods with + | None, _ -> prod :: prods + | Some _, [] -> raise Not_found + | Some ins_after_prod, hd :: tl -> + if ematch hd ins_after_prod then + (List.rev res) @ (hd :: prod :: tl) + else + insert_prod prev_prod prod tl (hd :: res) + in + + (* insert prods that are not already in og_prods *) + let rec upd_prods prev_prod eg_prods og_prods = + match eg_prods with + | [] -> og_prods + | prod :: tl -> + let og_prods = + if has_match prod og_prods then + List.map (fun p -> if ematch p prod then prod else p) og_prods + else + insert_prod prev_prod prod og_prods [] in + upd_prods (Some prod) tl og_prods + in + + (* add nts and prods not present in orderedGrammar *) + let _ = List.fold_left (fun prev_nt nt -> + let e_prods = NTMap.find nt !eg.map in + if not (NTMap.mem nt !og.map) then + g_add_after og prev_nt nt e_prods + else + g_update_prods og nt (upd_prods None e_prods (NTMap.find nt !og.map)); + Some nt) + None !eg.order in + g_reorder eg !og.map !og.order + + +let finish_with_file old_file verify = + let files_eq f1 f2 = + let chunksize = 8192 in + (try + let ofile = open_in_bin f1 in + let nfile = open_in_bin f2 in + let rv = if (in_channel_length ofile) <> (in_channel_length nfile) then false + else begin + let obuf = Bytes.create chunksize in + Bytes.fill obuf 0 chunksize '\x00'; + let nbuf = Bytes.create chunksize in + Bytes.fill nbuf 0 chunksize '\x00'; + let rec read () = + let olen = input ofile obuf 0 chunksize in + let _ = input nfile nbuf 0 chunksize in + if obuf <> nbuf then + false + else if olen = 0 then + true + else + read () + in + read () + end + in + close_in ofile; + close_in nfile; + rv + with Sys_error _ -> false) + in + + let temp_file = (old_file ^ "_temp") in + if verify then + if (files_eq old_file temp_file || !exit_code <> 0) then + Sys.remove temp_file + else + error "%s is not current\n" old_file + else + Sys.rename temp_file old_file + +let open_temp_bin file = + open_out_bin (sprintf "%s_temp" file) + +let find_longest_match prods str = + (* todo: require a minimum length? *) + let common_prefix_len s1 s2 = + let limit = min (String.length s1) (String.length s2) in + let rec aux off = + if off = limit then off + else if s1.[off] = s2.[off] then aux (succ off) + else off + in + aux 0 + in + + let slen = String.length str in + let rec longest best multi best_len prods = + match prods with + | [] -> best, multi, best_len + | prod :: tl -> + let pstr = String.trim (prod_to_prodn prod) in + let clen = common_prefix_len str pstr in + if clen = slen && slen = String.length pstr then + pstr, false, clen (* exact match *) + else if clen > best_len then + longest pstr false clen tl (* better match *) + else if clen = best_len then + longest best true best_len tl (* 2nd match with same length *) + else + longest best multi best_len tl (* worse match *) + in + longest "" false 0 prods + +type seen = { + nts: (string * int) NTMap.t; + tacs: (string * int) NTMap.t; + cmds: (string * int) NTMap.t; +} + +let process_rst g file args seen tac_prods cmd_prods = + let old_rst = open_in file in + let new_rst = open_temp_bin file in + let linenum = ref 0 in + let dir_regex = Str.regexp "^\\([ \t]*\\)\\.\\.[ \t]*\\([a-zA-Z0-9:]*\\)\\(.*\\)" in + let ig_args_regex = Str.regexp "^[ \t]*\\([a-zA-Z0-9_\\.]*\\)[ \t]*\\([a-zA-Z0-9_\\.]*\\)" in + let blank_regex = Str.regexp "^[ \t]*$" in + let end_prodlist_regex = Str.regexp "^[ \t]*$" in + let rec index_of_r str list index = + match list with + | [] -> None + | hd :: list -> + if hd = str then Some index + else index_of_r str list (index+1) + in + let index_of str list = index_of_r str list 0 in + let getline () = + let line = input_line old_rst in + incr linenum; + line + in + let output_insertgram start_index end_ indent is_coq_group = + let rec nthcdr n list = if n = 0 then list else nthcdr (n-1) (List.tl list) in + let rec copy_prods list = + match list with + | [] -> () + | nt :: tl -> + (try + let (prev_file, prev_linenum) = NTMap.find nt !seen.nts in + warn "%s line %d: '%s' already included at %s line %d\n" + file !linenum nt prev_file prev_linenum; + with Not_found -> + if is_coq_group then + seen := { !seen with nts = (NTMap.add nt (file, !linenum) !seen.nts)} ); + let prods = NTMap.find nt !g.map in + List.iteri (fun i prod -> + let rhs = String.trim (sprintf ": %s" (prod_to_str ~plist:true prod)) in + fprintf new_rst "%s %s %s\n" indent (if i = 0 then nt else String.make (String.length nt) ' ') rhs) + prods; + if nt <> end_ then copy_prods tl + in + copy_prods (nthcdr start_index !g.order) + in + + let process_insertgram line rhs = + if not (Str.string_match ig_args_regex rhs 0) then + error "%s line %d: bad arguments '%s' for 'insertgram'\n" file !linenum rhs + else begin + let start = Str.matched_group 1 rhs in + let end_ = Str.matched_group 2 rhs in + let start_index = index_of start !g.order in + let end_index = index_of end_ !g.order in + if start_index = None then + error "%s line %d: '%s' is undefined\n" file !linenum start; + if end_index = None then + error "%s line %d: '%s' is undefined\n" file !linenum end_; + match start_index, end_index with + | Some start_index, Some end_index -> + if start_index > end_index then + error "%s line %d: '%s' must appear before '%s' in .../orderedGrammar\n" file !linenum start end_ + else begin + try + let line2 = getline() in + if not (Str.string_match blank_regex line2 0) then + error "%s line %d: expecting a blank line after 'insertgram'\n" file !linenum + else begin + let line3 = getline() in + if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "productionlist::" then + error "%s line %d: expecting 'productionlist' after 'insertgram'\n" file !linenum + else begin + let indent = Str.matched_group 1 line3 in + let is_coq_group = ("coq" = String.trim (Str.matched_group 3 line3)) in + let rec skip_to_end () = + let endline = getline() in + if Str.string_match end_prodlist_regex endline 0 then begin + fprintf new_rst "%s\n\n%s\n" line line3; + output_insertgram start_index end_ indent is_coq_group; + fprintf new_rst "%s\n" endline + end else + skip_to_end () + in + skip_to_end () + end + end + with End_of_file -> error "%s line %d: unexpected end of file\n" file !linenum; + end + | _ -> () + end + + in + try + while true do + let line = getline() in + if Str.string_match dir_regex line 0 then begin + let dir = Str.matched_group 2 line in + let rhs = String.trim (Str.matched_group 3 line) in + match dir with + | "productionlist::" -> + if rhs = "coq" then + warn "%s line %d: Missing 'insertgram' before 'productionlist:: coq'\n" file !linenum; + fprintf new_rst "%s\n" line; + | "tacn::" when args.check_tacs -> + if not (StringSet.mem rhs tac_prods) then + warn "%s line %d: Unknown tactic: '%s'\n" file !linenum rhs; + if NTMap.mem rhs !seen.tacs then + warn "%s line %d: Repeated tactic: '%s'\n" file !linenum rhs; + seen := { !seen with tacs = (NTMap.add rhs (file, !linenum) !seen.tacs)}; + fprintf new_rst "%s\n" line + | "cmd::" when args.check_cmds -> + if not (StringSet.mem rhs cmd_prods) then + warn "%s line %d: Unknown command: '%s'\n" file !linenum rhs; + if NTMap.mem rhs !seen.cmds then + warn "%s line %d: Repeated command: '%s'\n" file !linenum rhs; + seen := { !seen with cmds = (NTMap.add rhs (file, !linenum) !seen.cmds)}; + fprintf new_rst "%s\n" line + | "insertgram" -> + process_insertgram line rhs + | _ -> fprintf new_rst "%s\n" line + end else + fprintf new_rst "%s\n" line; + done + with End_of_file -> (); + close_in old_rst; + close_out new_rst; + finish_with_file file args.verify + +let report_omitted_prods entries seen label split = + let maybe_warn first last n = + if first <> "" then begin + if first <> last then + warn "%ss '%s' to %s'%s' not included in .rst files (%d)\n" label first split last n + else + warn "%s %s not included in .rst files\n" label first; + end + in + + let first, last, n = List.fold_left (fun missing nt -> + let first, last, n = missing in + if NTMap.mem nt seen then begin + maybe_warn first last n; + "", "", 0 + end else + (if first = "" then nt else first), nt, n + 1) + ("", "", 0) entries in + maybe_warn first last n + +let process_grammar args = + let symdef_map = ref StringMap.empty in + let g = ref { map = NTMap.empty; order = [] } in + + let level_renames = read_mlg_files g args symdef_map in + + (* rename nts with levels *) + List.iter (fun b -> let (nt, prod) = b in + let (_, prod) = edit_rule g level_renames nt prod in + g_update_prods g nt prod) + (NTMap.bindings !g.map); + + (* print the full grammar with minimal editing *) + let out = open_temp_bin (dir "fullGrammar") in + fprintf out "%s\n%s\n\n" + "(* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *)" + "DOC_GRAMMAR"; + print_in_order out g `MLG !g.order StringSet.empty; + close_out out; + finish_with_file (dir "fullGrammar") args.verify; + if args.verbose then + print_special_tokens g; + + if not args.fullGrammar then begin + (* do shared edits *) + if !exit_code = 0 then begin + let common_edits = read_mlg_edit "common.edit_mlg" in + apply_edit_file g common_edits + end; + let prodn_gram = ref { map = !g.map; order = !g.order } in + + if !exit_code = 0 && not args.verify then begin + let prodlist_edits = read_mlg_edit "productionlist.edit_mlg" in + apply_edit_file g prodlist_edits; + let out = open_temp_bin (dir "productionlistGrammar") in + if args.verbose then + report_info g !symdef_map; + print_in_order out g `PRODLIST !g.order StringSet.empty; + (*print_chunks g out `PRODLIST ();*) + close_out out; + finish_with_file (dir "productionlistGrammar") args.verify; + end; + + if !exit_code = 0 && not args.verify then begin + let out = open_temp_bin (dir "editedGrammar") in + fprintf out "%s\n%s\n\n" + "(* Edited Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *)" + "DOC_GRAMMAR"; + print_in_order out g `MLG !g.order StringSet.empty; + close_out out; + finish_with_file (dir "editedGrammar") args.verify; + report_bad_nts g "editedGrammar" + end; + + if !exit_code = 0 then begin + let ordered_grammar = read_mlg_edit "orderedGrammar" in + let out = open_temp_bin (dir "orderedGrammar") in + fprintf out "%s\n%s\n\n" + ("(* Defines the order to apply to editedGrammar to get productionlistGrammar.\n" ^ + "doc_grammar will modify this file to add/remove nonterminals and productions\n" ^ + "to match editedGrammar, which will remove comments. Not compiled into Coq *)") + "DOC_GRAMMAR"; + reorder_grammar g ordered_grammar "orderedGrammar"; + print_in_order out g `MLG !g.order StringSet.empty; + close_out out; + finish_with_file (dir "orderedGrammar") args.verify; + end; + + if !exit_code = 0 then begin + let plist nt = + let list = (List.map (fun t -> String.trim (prod_to_prodn t)) + (NTMap.find nt !g.map)) in + list, StringSet.of_list list in + let tac_list, tac_prods = plist "simple_tactic" in + let cmd_list, cmd_prods = plist "command" in + let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; cmds=NTMap.empty } in + List.iter (fun file -> process_rst g file args seen tac_prods cmd_prods) args.rst_files; + report_omitted_prods !g.order !seen.nts "Nonterminal" ""; + if args.check_tacs then + report_omitted_prods tac_list !seen.tacs "Tactic" "\n "; + if args.check_cmds then + report_omitted_prods cmd_list !seen.cmds "Command" "\n " + end; + + (* generate output for prodn: simple_tactic, command, also for Ltac?? *) + if !exit_code = 0 && not args.verify then begin + let prodn_edits = read_mlg_edit "prodn.edit_mlg" in + apply_edit_file prodn_gram prodn_edits; + let out = open_temp_bin (dir "prodnGrammar") in + print_in_order out prodn_gram `PRODN !prodn_gram.order StringSet.empty; + close_out out; + finish_with_file (dir "prodnGrammar") args.verify + end + end + +let parse_args () = + let suffix_regex = Str.regexp ".*\\.\\([a-z]+\\)$" in + let args = + List.fold_left (fun args arg -> + match arg with + | "-check-cmds" -> { args with check_cmds = true } + | "-check-tacs" -> { args with check_tacs = true } + | "-no-warn" -> show_warn := false; { args with show_warn = true } + | "-short" -> { args with fullGrammar = true } + | "-verbose" -> { args with verbose = true } + | "-verify" -> { args with verify = true } + | arg when Str.string_match suffix_regex arg 0 -> + (match Str.matched_group 1 arg with + | "mlg" -> { args with mlg_files = (arg :: args.mlg_files) } + | "rst" -> { args with rst_files = (arg :: args.rst_files) } + | _ -> error "Unknown command line argument '%s'\n" arg; args) + | arg -> error "Unknown command line argument '%s'\n" arg; args) + default_args (List.tl (Array.to_list Sys.argv)) in + { args with mlg_files = (List.rev args.mlg_files); rst_files = (List.rev args.rst_files)} + +let () = + (*try*) + Printexc.record_backtrace true; + let args = parse_args () in + if !exit_code = 0 then begin + process_grammar args + end; + exit !exit_code + (*with _ -> Printexc.print_backtrace stdout; exit 1*) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar new file mode 100644 index 0000000000..a83638dd73 --- /dev/null +++ b/doc/tools/docgram/fullGrammar @@ -0,0 +1,3174 @@ +(* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *) +DOC_GRAMMAR + +Constr.ident: [ +| Prim.ident +] + +Prim.name: [ +| "_" +] + +global: [ +| Prim.reference +] + +constr_pattern: [ +| constr +] + +lconstr_pattern: [ +| lconstr +] + +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" +] + +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +] + +universe_increment: [ +| "+" natural +| +] + +universe_name: [ +| global +| "Set" +| "Prop" +] + +universe_expr: [ +| universe_name universe_increment +] + +universe: [ +| "max" "(" LIST1 universe_expr SEP "," ")" +| universe_expr +] + +lconstr: [ +| operconstr200 +| l_constr +] + +constr: [ +| operconstr8 +| "@" global instance +] + +operconstr200: [ +| binder_constr +| operconstr100 +] + +operconstr100: [ +| operconstr99 "<:" binder_constr +| operconstr99 "<:" operconstr100 +| operconstr99 "<<:" binder_constr +| operconstr99 "<<:" operconstr100 +| operconstr99 ":" binder_constr +| operconstr99 ":" operconstr100 +| operconstr99 ":>" +| operconstr99 +] + +operconstr99: [ +| operconstr90 +] + +operconstr90: [ +| operconstr10 +] + +operconstr10: [ +| operconstr9 LIST1 appl_arg +| "@" global instance LIST0 operconstr9 +| "@" pattern_identref LIST1 identref +| operconstr9 +] + +operconstr9: [ +| ".." operconstr0 ".." +| operconstr8 +] + +operconstr8: [ +| operconstr1 +] + +operconstr1: [ +| operconstr0 ".(" global LIST0 appl_arg ")" +| operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")" +| operconstr0 "%" IDENT +| operconstr0 +] + +operconstr0: [ +| atomic_constr +| match_constr +| "(" operconstr200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" operconstr200 "}" +| "`(" operconstr200 ")" +| "ltac" ":" "(" Pltac.tactic_expr ")" +] + +record_declaration: [ +| record_fields +] + +record_fields: [ +| record_field_declaration ";" record_fields +| record_field_declaration +| +| record_field ";" record_fields +| record_field ";" +| record_field +] + +record_field_declaration: [ +| global binders ":=" lconstr +] + +binder_constr: [ +| "forall" open_binders "," operconstr200 +| "fun" open_binders "=>" operconstr200 +| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200 +| "let" single_fix "in" operconstr200 +| "let" [ "(" LIST0 name SEP "," ")" | "()" ] return_type ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200 +| fix_constr +| "if" operconstr200 "is" ssr_dthen ssr_else (* ssr plugin *) +| "if" operconstr200 "isn't" ssr_dthen ssr_else (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +] + +appl_arg: [ +| lpar_id_coloneq lconstr ")" +| operconstr9 +] + +atomic_constr: [ +| global instance +| sort +| NUMERAL +| string +| "_" +| "?" "[" ident "]" +| "?" "[" pattern_ident "]" +| pattern_ident evar_instance +] + +inst: [ +| ident ":=" lconstr +] + +evar_instance: [ +| "@{" LIST1 inst SEP ";" "}" +| +] + +instance: [ +| "@{" LIST0 universe_level "}" +| +] + +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global +] + +fix_constr: [ +| single_fix +| single_fix "with" LIST1 fix_decl SEP "with" "for" identref +] + +single_fix: [ +| fix_kw fix_decl +] + +fix_kw: [ +| "fix" +| "cofix" +] + +fix_decl: [ +| identref binders_fixannot type_cstr ":=" operconstr200 +] + +match_constr: [ +| "match" LIST1 case_item SEP "," OPT case_type "with" branches "end" +] + +case_item: [ +| operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ] +] + +case_type: [ +| "return" operconstr100 +] + +return_type: [ +| OPT [ OPT [ "as" name ] case_type ] +] + +branches: [ +| OPT "|" LIST0 eqn SEP "|" +] + +mult_pattern: [ +| LIST1 pattern200 SEP "," +] + +eqn: [ +| LIST1 mult_pattern SEP "|" "=>" lconstr +] + +record_pattern: [ +| global ":=" pattern200 +] + +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern ";" +| record_pattern +| +] + +pattern200: [ +| pattern100 +] + +pattern100: [ +| pattern99 ":" binder_constr +| pattern99 ":" operconstr100 +| pattern99 +] + +pattern99: [ +| pattern90 +] + +pattern90: [ +| pattern10 +] + +pattern10: [ +| pattern1 "as" name +| pattern1 LIST1 pattern1 +| "@" Prim.reference LIST0 pattern1 +| pattern1 +] + +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| Prim.reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" LIST1 pattern200 SEP "|" ")" +| NUMERAL +| string +] + +impl_ident_tail: [ +| "}" +| LIST1 name ":" lconstr "}" +| LIST1 name "}" +| ":" lconstr "}" +] + +fixannot: [ +| "{" "struct" identref "}" +| "{" "wf" constr identref "}" +| "{" "measure" constr OPT identref OPT constr "}" +| "{" "struct" name "}" +| +] + +impl_name_head: [ +| impl_ident_head +] + +binders_fixannot: [ +| impl_name_head impl_ident_tail binders_fixannot +| fixannot +| binder binders_fixannot +| +] + +open_binders: [ +| name LIST0 name ":" lconstr +| name LIST0 name binders +| name ".." name +| closed_binder binders +] + +binders: [ +| LIST0 binder +| Pcoq.Constr.binders +] + +binder: [ +| name +| closed_binder +] + +closed_binder: [ +| "(" name LIST1 name ":" lconstr ")" +| "(" name ":" lconstr ")" +| "(" name ":=" lconstr ")" +| "(" name ":" lconstr ":=" lconstr ")" +| "{" name "}" +| "{" name LIST1 name ":" lconstr "}" +| "{" name ":" lconstr "}" +| "{" name LIST1 name "}" +| "`(" LIST1 typeclass_constraint SEP "," ")" +| "`{" LIST1 typeclass_constraint SEP "," "}" +| "'" pattern0 +| [ "of" | "&" ] operconstr99 (* ssr plugin *) +] + +typeclass_constraint: [ +| "!" operconstr200 +| "{" name "}" ":" [ "!" | ] operconstr200 +| name_colon [ "!" | ] operconstr200 +| operconstr200 +] + +type_cstr: [ +| OPT [ ":" lconstr ] +| ":" lconstr +| +] + +preident: [ +| IDENT +] + +ident: [ +| IDENT +] + +pattern_ident: [ +| LEFTQMARK ident +] + +pattern_identref: [ +| pattern_ident +] + +var: [ +| ident +] + +identref: [ +| ident +] + +field: [ +| FIELD +] + +fields: [ +| field fields +| field +] + +fullyqualid: [ +| ident fields +| ident +] + +basequalid: [ +| ident fields +| ident +] + +name: [ +| "_" +| ident +] + +reference: [ +| ident fields +| ident +] + +by_notation: [ +| ne_string OPT [ "%" IDENT ] +] + +smart_global: [ +| reference +| by_notation +] + +qualid: [ +| basequalid +] + +ne_string: [ +| STRING +] + +ne_lstring: [ +| ne_string +] + +dirpath: [ +| ident LIST0 field +] + +string: [ +| STRING +] + +lstring: [ +| string +] + +integer: [ +| NUMERAL +| "-" NUMERAL +] + +natural: [ +| NUMERAL +| _natural +] + +bigint: [ +| NUMERAL +] + +bar_cbrace: [ +| "|" "}" +] + +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "Backtrack" natural natural natural "." +| test_show_goal "Show" "Goal" natural "at" natural "." +| Pvernac.Vernac_.main_entry +] + +opt_hintbases: [ +| +| ":" LIST1 IDENT +] + +command: [ +| "Goal" lconstr +| "Proof" +| "Proof" "Mode" string +| "Proof" lconstr +| "Abort" +| "Abort" "All" +| "Abort" identref +| "Existential" natural constr_body +| "Admitted" +| "Qed" +| "Save" identref +| "Defined" +| "Defined" identref +| "Restart" +| "Undo" +| "Undo" natural +| "Undo" "To" natural +| "Focus" +| "Focus" natural +| "Unfocus" +| "Unfocused" +| "Show" +| "Show" natural +| "Show" ident +| "Show" "Existentials" +| "Show" "Universes" +| "Show" "Conjectures" +| "Show" "Proof" +| "Show" "Intro" +| "Show" "Intros" +| "Show" "Match" reference +| "Guarded" +| "Create" "HintDb" IDENT; [ "discriminated" | ] +| "Remove" "Hints" LIST1 global opt_hintbases +| "Hint" hint opt_hintbases +| "Comments" LIST0 comment +| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info +| "Declare" "Scope" IDENT +| "Pwd" +| "Cd" +| "Cd" ne_string +| "Load" [ "Verbose" | ] [ ne_string | IDENT ] +| "Declare" "ML" "Module" LIST1 ne_string +| "Locate" locatable +| "Add" "LoadPath" ne_string as_dirpath +| "Add" "Rec" "LoadPath" ne_string as_dirpath +| "Remove" "LoadPath" ne_string +| "AddPath" ne_string "as" as_dirpath +| "AddRecPath" ne_string "as" as_dirpath +| "DelPath" ne_string +| "Type" lconstr +| "Print" printable +| "Print" smart_global OPT univ_name_list +| "Print" "Module" "Type" global +| "Print" "Module" global +| "Print" "Namespace" dirpath +| "Inspect" natural +| "Add" "ML" "Path" ne_string +| "Add" "Rec" "ML" "Path" ne_string +| "Set" option_table option_setting +| "Unset" option_table +| "Print" "Table" option_table +| "Add" IDENT IDENT LIST1 option_ref_value +| "Add" IDENT LIST1 option_ref_value +| "Test" option_table "for" LIST1 option_ref_value +| "Test" option_table +| "Remove" IDENT IDENT LIST1 option_ref_value +| "Remove" IDENT LIST1 option_ref_value +| "Write" "State" IDENT +| "Write" "State" ne_string +| "Restore" "State" IDENT +| "Restore" "State" ne_string +| "Reset" "Initial" +| "Reset" identref +| "Back" +| "Back" natural +| "BackTo" natural +| "Debug" "On" +| "Debug" "Off" +| "Declare" "Reduction" IDENT; ":=" red_expr +| "Declare" "Custom" "Entry" IDENT +| "Derive" ident "SuchThat" constr "As" ident (* derive plugin *) +| "Extraction" global (* extraction plugin *) +| "Recursive" "Extraction" LIST1 global (* extraction plugin *) +| "Extraction" string LIST1 global (* extraction plugin *) +| "Extraction" "TestCompile" LIST1 global (* extraction plugin *) +| "Separate" "Extraction" LIST1 global (* extraction plugin *) +| "Extraction" "Library" ident (* extraction plugin *) +| "Recursive" "Extraction" "Library" ident (* extraction plugin *) +| "Extraction" "Language" language (* extraction plugin *) +| "Extraction" "Inline" LIST1 global (* extraction plugin *) +| "Extraction" "NoInline" LIST1 global (* extraction plugin *) +| "Print" "Extraction" "Inline" (* extraction plugin *) +| "Reset" "Extraction" "Inline" (* extraction plugin *) +| "Extraction" "Implicit" global "[" LIST0 int_or_id "]" (* extraction plugin *) +| "Extraction" "Blacklist" LIST1 ident (* extraction plugin *) +| "Print" "Extraction" "Blacklist" (* extraction plugin *) +| "Reset" "Extraction" "Blacklist" (* extraction plugin *) +| "Extract" "Constant" global LIST0 string "=>" mlname (* extraction plugin *) +| "Extract" "Inlined" "Constant" global "=>" mlname (* extraction plugin *) +| "Extract" "Inductive" global "=>" mlname "[" LIST0 mlname "]" OPT string (* extraction plugin *) +| "Show" "Extraction" (* extraction plugin *) +| "Set" "Firstorder" "Solver" tactic +| "Print" "Firstorder" "Solver" +| "Function" LIST1 function_rec_definition_loc SEP "with" (* funind plugin *) +| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) +| "Functional" "Case" fun_scheme_arg (* funind plugin *) +| "Generate" "graph" "for" reference (* funind plugin *) +| "Hint" "Rewrite" orient LIST1 constr ":" LIST0 preident +| "Hint" "Rewrite" orient LIST1 constr "using" tactic ":" LIST0 preident +| "Hint" "Rewrite" orient LIST1 constr +| "Hint" "Rewrite" orient LIST1 constr "using" tactic +| "Derive" "Inversion_clear" ident "with" constr "Sort" sort_family +| "Derive" "Inversion_clear" ident "with" constr +| "Derive" "Inversion" ident "with" constr "Sort" sort_family +| "Derive" "Inversion" ident "with" constr +| "Derive" "Dependent" "Inversion" ident "with" constr "Sort" sort_family +| "Derive" "Dependent" "Inversion_clear" ident "with" constr "Sort" sort_family +| "Declare" "Left" "Step" constr +| "Declare" "Right" "Step" constr +| "Grab" "Existential" "Variables" +| "Unshelve" +| "Declare" "Equivalent" "Keys" constr constr +| "Print" "Equivalent" "Keys" +| "Optimize" "Proof" +| "Optimize" "Heap" +| "Hint" "Cut" "[" hints_path "]" opthints +| "Typeclasses" "Transparent" LIST0 reference +| "Typeclasses" "Opaque" LIST0 reference +| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int +| "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] +| "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ] +| "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic +| "Print" "Ltac" reference +| "Locate" "Ltac" reference +| "Ltac" LIST1 ltac_tacdef_body SEP "with" +| "Print" "Ltac" "Signatures" +| "Obligation" integer "of" ident ":" lglob withtac +| "Obligation" integer "of" ident withtac +| "Obligation" integer ":" lglob withtac +| "Obligation" integer withtac +| "Next" "Obligation" "of" ident withtac +| "Next" "Obligation" withtac +| "Solve" "Obligation" integer "of" ident "with" tactic +| "Solve" "Obligation" integer "with" tactic +| "Solve" "Obligations" "of" ident "with" tactic +| "Solve" "Obligations" "with" tactic +| "Solve" "Obligations" +| "Solve" "All" "Obligations" "with" tactic +| "Solve" "All" "Obligations" +| "Admit" "Obligations" "of" ident +| "Admit" "Obligations" +| "Obligation" "Tactic" ":=" tactic +| "Show" "Obligation" "Tactic" +| "Obligations" "of" ident +| "Obligations" +| "Preterm" "of" ident +| "Preterm" +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "as" ident +| "Add" "Relation" constr constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Relation" constr constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Parametric" "Relation" binders ":" constr constr "transitivity" "proved" "by" constr "as" ident +| "Add" "Setoid" constr constr constr "as" ident +| "Add" "Parametric" "Setoid" binders ":" constr constr constr "as" ident +| "Add" "Morphism" constr ":" ident +| "Declare" "Morphism" constr ":" ident +| "Add" "Morphism" constr "with" "signature" lconstr "as" ident +| "Add" "Parametric" "Morphism" binders ":" constr "with" "signature" lconstr "as" ident +| "Print" "Rewrite" "HintDb" preident +| "Reset" "Ltac" "Profile" +| "Show" "Ltac" "Profile" +| "Show" "Ltac" "Profile" "CutOff" int +| "Show" "Ltac" "Profile" string +| "Add" "Ring" ident ":" constr OPT ring_mods (* setoid_ring plugin *) +| "Print" "Rings" (* setoid_ring plugin *) +| "Add" "Field" ident ":" constr OPT field_mods (* setoid_ring plugin *) +| "Print" "Fields" (* setoid_ring plugin *) +| "Prenex" "Implicits" LIST1 global (* ssr plugin *) +| "Search" ssr_search_arg ssr_modlocs (* ssr plugin *) +| "Print" "Hint" "View" ssrviewpos (* ssr plugin *) +| "Hint" "View" ssrviewposspc LIST1 ssrhintref (* ssr plugin *) +| "Numeral" "Notation" reference reference reference ":" ident numnotoption +| "String" "Notation" reference reference reference ":" ident +] + +reference_or_constr: [ +| global +| constr +] + +hint: [ +| "Resolve" LIST1 reference_or_constr hint_info +| "Resolve" "->" LIST1 global OPT natural +| "Resolve" "<-" LIST1 global OPT natural +| "Immediate" LIST1 reference_or_constr +| "Variables" "Transparent" +| "Variables" "Opaque" +| "Constants" "Transparent" +| "Constants" "Opaque" +| "Transparent" LIST1 global +| "Opaque" LIST1 global +| "Mode" global mode +| "Unfold" LIST1 global +| "Constructors" LIST1 global +| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic +] + +constr_body: [ +| ":=" lconstr +| ":" lconstr ":=" lconstr +] + +mode: [ +| LIST1 [ "+" | "!" | "-" ] +] + +vernac_control: [ +| "Time" vernac_control +| "Redirect" ne_string vernac_control +| "Timeout" natural vernac_control +| "Fail" vernac_control +| decorated_vernac +] + +decorated_vernac: [ +| LIST0 quoted_attributes vernac +] + +quoted_attributes: [ +| "#[" attribute_list "]" +] + +attribute_list: [ +| LIST0 attribute SEP "," +] + +attribute: [ +| ident attribute_value +] + +attribute_value: [ +| "=" string +| "(" attribute_list ")" +| +] + +vernac: [ +| "Local" vernac_poly +| "Global" vernac_poly +| vernac_poly +] + +vernac_poly: [ +| "Polymorphic" vernac_aux +| "Monomorphic" vernac_aux +| vernac_aux +] + +vernac_aux: [ +| "Program" gallina "." +| "Program" gallina_ext "." +| gallina "." +| gallina_ext "." +| command "." +| syntax "." +| subprf +| command_entry +] + +noedit_mode: [ +| query_command +] + +subprf: [ +| BULLET +| "{" +| "}" +] + +gallina: [ +| thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ] +| assumption_token inline assum_list +| assumptions_token inline assum_list +| def_token ident_decl def_body +| "Let" identref def_body +| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| "Fixpoint" LIST1 rec_definition SEP "with" +| "Let" "Fixpoint" LIST1 rec_definition SEP "with" +| "CoFixpoint" LIST1 corec_definition SEP "with" +| "Let" "CoFixpoint" LIST1 corec_definition SEP "with" +| "Scheme" LIST1 scheme SEP "with" +| "Combined" "Scheme" identref "from" LIST1 identref SEP "," +| "Register" global "as" qualid +| "Register" "Inline" global +| "Primitive" identref OPT [ ":" lconstr ] ":=" register_token +| "Universe" LIST1 identref +| "Universes" LIST1 identref +| "Constraint" LIST1 univ_constraint SEP "," +] + +register_token: [ +| register_prim_token +| register_type_token +] + +register_type_token: [ +| "#int63_type" +] + +register_prim_token: [ +| "#int63_head0" +| "#int63_tail0" +| "#int63_add" +| "#int63_sub" +| "#int63_mul" +| "#int63_div" +| "#int63_mod" +| "#int63_lsr" +| "#int63_lsl" +| "#int63_land" +| "#int63_lor" +| "#int63_lxor" +| "#int63_addc" +| "#int63_subc" +| "#int63_addcarryc" +| "#int63_subcarryc" +| "#int63_mulc" +| "#int63_diveucl" +| "#int63_div21" +| "#int63_addmuldiv" +| "#int63_eq" +| "#int63_lt" +| "#int63_le" +| "#int63_compare" +] + +thm_token: [ +| "Theorem" +| "Lemma" +| "Fact" +| "Remark" +| "Corollary" +| "Proposition" +| "Property" +] + +def_token: [ +| "Definition" +| "Example" +| "SubClass" +] + +assumption_token: [ +| "Hypothesis" +| "Variable" +| "Axiom" +| "Parameter" +| "Conjecture" +] + +assumptions_token: [ +| "Hypotheses" +| "Variables" +| "Axioms" +| "Parameters" +| "Conjectures" +] + +inline: [ +| "Inline" "(" natural ")" +| "Inline" +| +] + +univ_constraint: [ +| universe_name [ "<" | "=" | "<=" ] universe_name +] + +univ_decl: [ +| "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] +] + +ident_decl: [ +| identref OPT univ_decl +] + +finite_token: [ +| "Inductive" +| "CoInductive" +| "Variant" +| "Record" +| "Structure" +| "Class" +] + +cumulativity_token: [ +| "Cumulative" +| "NonCumulative" +] + +private_token: [ +| "Private" +| +] + +def_body: [ +| binders ":=" reduce lconstr +| binders ":" lconstr ":=" reduce lconstr +| binders ":" lconstr +] + +reduce: [ +| "Eval" red_expr "in" +| +] + +one_decl_notation: [ +| ne_lstring ":=" constr OPT [ ":" IDENT ] +] + +decl_sep: [ +| "and" +] + +decl_notation: [ +| "where" LIST1 one_decl_notation SEP decl_sep +| +] + +opt_constructors_or_fields: [ +| ":=" constructor_list_or_record_decl +| +] + +inductive_definition: [ +| opt_coercion ident_decl binders OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation +] + +constructor_list_or_record_decl: [ +| "|" LIST1 constructor SEP "|" +| identref constructor_type "|" LIST0 constructor SEP "|" +| identref constructor_type +| identref "{" record_fields "}" +| "{" record_fields "}" +| +] + +opt_coercion: [ +| ">" +| +] + +rec_definition: [ +| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation +] + +corec_definition: [ +| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation +] + +scheme: [ +| scheme_kind +| identref ":=" scheme_kind +] + +scheme_kind: [ +| "Induction" "for" smart_global "Sort" sort_family +| "Minimality" "for" smart_global "Sort" sort_family +| "Elimination" "for" smart_global "Sort" sort_family +| "Case" "for" smart_global "Sort" sort_family +| "Equality" "for" smart_global +] + +record_field: [ +| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notation +] + +record_binder_body: [ +| binders of_type_with_opt_coercion lconstr +| binders of_type_with_opt_coercion lconstr ":=" lconstr +| binders ":=" lconstr +] + +record_binder: [ +| name +| name record_binder_body +] + +assum_list: [ +| LIST1 assum_coe +| simple_assum_coe +] + +assum_coe: [ +| "(" simple_assum_coe ")" +] + +simple_assum_coe: [ +| LIST1 ident_decl of_type_with_opt_coercion lconstr +] + +constructor_type: [ +| binders [ of_type_with_opt_coercion lconstr | ] +] + +constructor: [ +| identref constructor_type +] + +of_type_with_opt_coercion: [ +| ":>>" +| ":>" ">" +| ":>" +| ":" ">" ">" +| ":" ">" +| ":" +] + +gallina_ext: [ +| "Module" export_token identref LIST0 module_binder of_module_type is_module_expr +| "Module" "Type" identref LIST0 module_binder check_module_types is_module_type +| "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl +| "Section" identref +| "Chapter" identref +| "End" identref +| "Collection" identref ":=" section_subset_expr +| "Require" export_token LIST1 global +| "From" global "Require" export_token LIST1 global +| "Import" LIST1 global +| "Export" LIST1 global +| "Include" module_type_inl LIST0 ext_module_expr +| "Include" "Type" module_type_inl LIST0 ext_module_type +| "Transparent" LIST1 smart_global +| "Opaque" LIST1 smart_global +| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ] +| "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ] +| "Canonical" OPT "Structure" by_notation +| "Coercion" global OPT univ_decl def_body +| "Identity" "Coercion" identref ":" class_rawexpr ">->" class_rawexpr +| "Coercion" global ":" class_rawexpr ">->" class_rawexpr +| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr +| "Context" LIST1 binder +| "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ] +| "Existing" "Instance" global hint_info +| "Existing" "Instances" LIST1 global OPT [ "|" natural ] +| "Existing" "Class" global +| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| "Implicit" "Type" reserv_list +| "Implicit" "Types" reserv_list +| "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ] +| "Export" "Set" option_table option_setting +| "Export" "Unset" option_table +| "Import" "Prenex" "Implicits" (* ssr plugin *) +] + +export_token: [ +| "Import" +| "Export" +| +] + +ext_module_type: [ +| "<+" module_type_inl +] + +ext_module_expr: [ +| "<+" module_expr_inl +] + +check_module_type: [ +| "<:" module_type_inl +] + +check_module_types: [ +| LIST0 check_module_type +] + +of_module_type: [ +| ":" module_type_inl +| check_module_types +] + +is_module_type: [ +| ":=" module_type_inl LIST0 ext_module_type +| +] + +is_module_expr: [ +| ":=" module_expr_inl LIST0 ext_module_expr +| +] + +functor_app_annot: [ +| "[" "inline" "at" "level" natural "]" +| "[" "no" "inline" "]" +| +] + +module_expr_inl: [ +| "!" module_expr +| module_expr functor_app_annot +] + +module_type_inl: [ +| "!" module_type +| module_type functor_app_annot +] + +module_binder: [ +| "(" export_token LIST1 identref ":" module_type_inl ")" +] + +module_expr: [ +| module_expr_atom +| module_expr module_expr_atom +] + +module_expr_atom: [ +| qualid +| "(" module_expr ")" +] + +with_declaration: [ +| "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr +| "Module" fullyqualid ":=" qualid +] + +module_type: [ +| qualid +| "(" module_type ")" +| module_type module_expr_atom +| module_type "with" with_declaration +] + +section_subset_expr: [ +| only_starredidentrefs LIST0 starredidentref +| ssexpr35 +] + +starredidentref: [ +| identref +| identref "*" +| "Type" +| "Type" "*" +] + +ssexpr35: [ +| "-" ssexpr50 +| ssexpr50 +] + +ssexpr50: [ +| ssexpr0 "-" ssexpr0 +| ssexpr0 "+" ssexpr0 +| ssexpr0 +] + +ssexpr0: [ +| starredidentref +| "(" only_starredidentrefs LIST0 starredidentref ")" +| "(" only_starredidentrefs LIST0 starredidentref ")" "*" +| "(" ssexpr35 ")" +| "(" ssexpr35 ")" "*" +] + +arguments_modifier: [ +| "simpl" "nomatch" +| "simpl" "never" +| "default" "implicits" +| "clear" "implicits" +| "clear" "scopes" +| "clear" "bidirectionality" "hint" +| "rename" +| "assert" +| "extra" "scopes" +| "clear" "scopes" "and" "implicits" +| "clear" "implicits" "and" "scopes" +] + +scope: [ +| "%" IDENT +] + +argument_spec: [ +| OPT "!" name OPT scope +] + +argument_spec_block: [ +| argument_spec +| "/" +| "&" +| "(" LIST1 argument_spec ")" OPT scope +| "[" LIST1 argument_spec "]" OPT scope +| "{" LIST1 argument_spec "}" OPT scope +] + +more_implicits_block: [ +| name +| "[" LIST1 name "]" +| "{" LIST1 name "}" +] + +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +] + +instance_name: [ +| ident_decl binders +| +] + +hint_info: [ +| "|" OPT natural OPT constr_pattern +| +] + +reserv_list: [ +| LIST1 reserv_tuple +| simple_reserv +] + +reserv_tuple: [ +| "(" simple_reserv ")" +] + +simple_reserv: [ +| LIST1 identref ":" lconstr +] + +query_command: [ +| "Eval" red_expr "in" lconstr "." +| "Compute" lconstr "." +| "Check" lconstr "." +| "About" smart_global OPT univ_name_list "." +| "SearchHead" constr_pattern in_or_out_modules "." +| "SearchPattern" constr_pattern in_or_out_modules "." +| "SearchRewrite" constr_pattern in_or_out_modules "." +| "Search" searchabout_query searchabout_queries "." +| "SearchAbout" searchabout_query searchabout_queries "." +| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." +] + +printable: [ +| "Term" smart_global OPT univ_name_list +| "All" +| "Section" global +| "Grammar" IDENT +| "Custom" "Grammar" IDENT +| "LoadPath" OPT dirpath +| "Modules" +| "Libraries" +| "ML" "Path" +| "ML" "Modules" +| "Debug" "GC" +| "Graph" +| "Classes" +| "TypeClasses" +| "Instances" smart_global +| "Coercions" +| "Coercion" "Paths" class_rawexpr class_rawexpr +| "Canonical" "Projections" +| "Tables" +| "Options" +| "Hint" +| "Hint" smart_global +| "Hint" "*" +| "HintDb" IDENT +| "Scopes" +| "Scope" IDENT +| "Visibility" OPT IDENT +| "Implicit" smart_global +| [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string +| "Assumptions" smart_global +| "Opaque" "Dependencies" smart_global +| "Transparent" "Dependencies" smart_global +| "All" "Dependencies" smart_global +| "Strategy" smart_global +| "Strategies" +| "Registered" +] + +printunivs_subgraph: [ +| "Subgraph" "(" LIST0 reference ")" +] + +class_rawexpr: [ +| "Funclass" +| "Sortclass" +| smart_global +] + +locatable: [ +| smart_global +| "Term" smart_global +| "File" ne_string +| "Library" global +| "Module" global +] + +option_setting: [ +| +| integer +| STRING +] + +option_ref_value: [ +| global +| STRING +] + +option_table: [ +| LIST1 IDENT +] + +as_dirpath: [ +| OPT [ "as" dirpath ] +] + +ne_in_or_out_modules: [ +| "inside" LIST1 global +| "outside" LIST1 global +] + +in_or_out_modules: [ +| ne_in_or_out_modules +| +] + +comment: [ +| constr +| STRING +| natural +] + +positive_search_mark: [ +| "-" +| +] + +searchabout_query: [ +| positive_search_mark ne_string OPT scope +| positive_search_mark constr_pattern +] + +searchabout_queries: [ +| ne_in_or_out_modules +| searchabout_query searchabout_queries +| +] + +univ_name_list: [ +| "@{" LIST0 name "}" +] + +syntax: [ +| "Open" "Scope" IDENT +| "Close" "Scope" IDENT +| "Delimit" "Scope" IDENT; "with" IDENT +| "Undelimit" "Scope" IDENT +| "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr +| "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] +| "Notation" identref LIST0 ident ":=" constr only_parsing +| "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] +| "Format" "Notation" STRING STRING STRING +| "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] +| "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] +] + +only_parsing: [ +| "(" "only" "parsing" ")" +| "(" "compat" STRING ")" +| +] + +level: [ +| "level" natural +| "next" "level" +] + +syntax_modifier: [ +| "at" "level" natural +| "in" "custom" IDENT +| "in" "custom" IDENT; "at" "level" natural +| "left" "associativity" +| "right" "associativity" +| "no" "associativity" +| "only" "printing" +| "only" "parsing" +| "compat" STRING +| "format" STRING OPT STRING +| IDENT; "," LIST1 IDENT SEP "," "at" level +| IDENT; "at" level +| IDENT; "at" level constr_as_binder_kind +| IDENT constr_as_binder_kind +| IDENT syntax_extension_type +] + +syntax_extension_type: [ +| "ident" +| "global" +| "bigint" +| "binder" +| "constr" +| "constr" OPT at_level OPT constr_as_binder_kind +| "pattern" +| "pattern" "at" "level" natural +| "strict" "pattern" +| "strict" "pattern" "at" "level" natural +| "closed" "binder" +| "custom" IDENT OPT at_level OPT constr_as_binder_kind +] + +at_level: [ +| "at" level +] + +constr_as_binder_kind: [ +| "as" "ident" +| "as" "pattern" +| "as" "strict" "pattern" +] + +simple_tactic: [ +| "btauto" +| "congruence" +| "congruence" integer +| "congruence" "with" LIST1 constr +| "congruence" integer "with" LIST1 constr +| "f_equal" +| "firstorder" OPT tactic firstorder_using +| "firstorder" OPT tactic "with" LIST1 preident +| "firstorder" OPT tactic firstorder_using "with" LIST1 preident +| "gintuition" OPT tactic +| "functional" "inversion" quantified_hypothesis OPT reference (* funind plugin *) +| "functional" "induction" LIST1 constr fun_ind_using with_names (* funind plugin *) +| "soft" "functional" "induction" LIST1 constr fun_ind_using with_names (* funind plugin *) +| "reflexivity" +| "exact" casted_constr +| "assumption" +| "etransitivity" +| "cut" constr +| "exact_no_check" constr +| "vm_cast_no_check" constr +| "native_cast_no_check" constr +| "casetype" constr +| "elimtype" constr +| "lapply" constr +| "transitivity" constr +| "left" +| "eleft" +| "left" "with" bindings +| "eleft" "with" bindings +| "right" +| "eright" +| "right" "with" bindings +| "eright" "with" bindings +| "constructor" +| "constructor" int_or_var +| "constructor" int_or_var "with" bindings +| "econstructor" +| "econstructor" int_or_var +| "econstructor" int_or_var "with" bindings +| "specialize" constr_with_bindings +| "specialize" constr_with_bindings "as" simple_intropattern +| "symmetry" +| "symmetry" "in" in_clause +| "split" +| "esplit" +| "split" "with" bindings +| "esplit" "with" bindings +| "exists" +| "exists" LIST1 bindings SEP "," +| "eexists" +| "eexists" LIST1 bindings SEP "," +| "intros" "until" quantified_hypothesis +| "intro" +| "intro" ident +| "intro" ident "at" "top" +| "intro" ident "at" "bottom" +| "intro" ident "after" hyp +| "intro" ident "before" hyp +| "intro" "at" "top" +| "intro" "at" "bottom" +| "intro" "after" hyp +| "intro" "before" hyp +| "move" hyp "at" "top" +| "move" hyp "at" "bottom" +| "move" hyp "after" hyp +| "move" hyp "before" hyp +| "rename" LIST1 rename SEP "," +| "revert" LIST1 hyp +| "simple" "induction" quantified_hypothesis +| "simple" "destruct" quantified_hypothesis +| "double" "induction" quantified_hypothesis quantified_hypothesis +| "admit" +| "fix" ident natural +| "cofix" ident +| "clear" LIST0 hyp +| "clear" "-" LIST1 hyp +| "clearbody" LIST1 hyp +| "generalize" "dependent" constr +| "replace" uconstr "with" constr clause by_arg_tac +| "replace" "->" uconstr clause +| "replace" "<-" uconstr clause +| "replace" uconstr clause +| "simplify_eq" +| "simplify_eq" destruction_arg +| "esimplify_eq" +| "esimplify_eq" destruction_arg +| "discriminate" +| "discriminate" destruction_arg +| "ediscriminate" +| "ediscriminate" destruction_arg +| "injection" +| "injection" destruction_arg +| "einjection" +| "einjection" destruction_arg +| "injection" "as" LIST0 simple_intropattern +| "injection" destruction_arg "as" LIST0 simple_intropattern +| "einjection" "as" LIST0 simple_intropattern +| "einjection" destruction_arg "as" LIST0 simple_intropattern +| "simple" "injection" +| "simple" "injection" destruction_arg +| "dependent" "rewrite" orient constr +| "dependent" "rewrite" orient constr "in" hyp +| "cutrewrite" orient constr +| "cutrewrite" orient constr "in" hyp +| "decompose" "sum" constr +| "decompose" "record" constr +| "absurd" constr +| "contradiction" OPT constr_with_bindings +| "autorewrite" "with" LIST1 preident clause +| "autorewrite" "with" LIST1 preident clause "using" tactic +| "autorewrite" "*" "with" LIST1 preident clause +| "autorewrite" "*" "with" LIST1 preident clause "using" tactic +| "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences "in" hyp by_arg_tac +| "rewrite" "*" orient uconstr "in" hyp by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr by_arg_tac +| "refine" uconstr +| "simple" "refine" uconstr +| "notypeclasses" "refine" uconstr +| "simple" "notypeclasses" "refine" uconstr +| "solve_constraints" +| "subst" LIST1 var +| "subst" +| "simple" "subst" +| "evar" test_lpar_id_colon "(" ident ":" lconstr ")" +| "evar" constr +| "instantiate" "(" ident ":=" lglob ")" +| "instantiate" "(" integer ":=" lglob ")" hloc +| "instantiate" +| "stepl" constr "by" tactic +| "stepl" constr +| "stepr" constr "by" tactic +| "stepr" constr +| "generalize_eqs" hyp +| "dependent" "generalize_eqs" hyp +| "generalize_eqs_vars" hyp +| "dependent" "generalize_eqs_vars" hyp +| "specialize_eqs" hyp +| "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr +| "hresolve_core" "(" ident ":=" constr ")" "in" constr +| "hget_evar" int_or_var +| "destauto" +| "destauto" "in" hyp +| "transparent_abstract" tactic3 +| "transparent_abstract" tactic3 "using" ident +| "constr_eq" constr constr +| "constr_eq_strict" constr constr +| "constr_eq_nounivs" constr constr +| "is_evar" constr +| "has_evar" constr +| "is_var" constr +| "is_fix" constr +| "is_cofix" constr +| "is_ind" constr +| "is_constructor" constr +| "is_proj" constr +| "is_const" constr +| "shelve" +| "shelve_unifiable" +| "unshelve" tactic1 +| "give_up" +| "cycle" int_or_var +| "swap" int_or_var int_or_var +| "revgoals" +| "guard" test +| "decompose" "[" LIST1 constr "]" constr +| "optimize_heap" +| "eassumption" +| "eexact" constr +| "trivial" auto_using hintbases +| "info_trivial" auto_using hintbases +| "debug" "trivial" auto_using hintbases +| "auto" OPT int_or_var auto_using hintbases +| "info_auto" OPT int_or_var auto_using hintbases +| "debug" "auto" OPT int_or_var auto_using hintbases +| "prolog" "[" LIST0 uconstr "]" int_or_var +| "eauto" OPT int_or_var OPT int_or_var auto_using hintbases +| "new" "auto" OPT int_or_var auto_using hintbases +| "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases +| "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases +| "dfs" "eauto" OPT int_or_var auto_using hintbases +| "autounfold" hintbases clause_dft_concl +| "autounfold_one" hintbases "in" hyp +| "autounfold_one" hintbases +| "unify" constr constr +| "unify" constr constr "with" preident +| "convert_concl_no_check" constr +| "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident +| "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident +| "typeclasses" "eauto" OPT int_or_var +| "head_of_constr" ident constr +| "not_evar" constr +| "is_ground" constr +| "autoapply" constr "using" preident +| "autoapply" constr "with" preident +| "progress_evars" tactic +| "decide" "equality" +| "compare" constr constr +| "rewrite_strat" rewstrategy "in" hyp +| "rewrite_strat" rewstrategy +| "rewrite_db" preident "in" hyp +| "rewrite_db" preident +| "substitute" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings "in" hyp +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" hyp +| "setoid_rewrite" orient glob_constr_with_bindings "in" hyp "at" occurrences +| "setoid_symmetry" +| "setoid_symmetry" "in" hyp +| "setoid_reflexivity" +| "setoid_transitivity" constr +| "setoid_etransitivity" +| "intros" ne_intropatterns +| "intros" +| "eintros" ne_intropatterns +| "eintros" +| "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," in_hyp_as +| "elim" constr_with_bindings_arg OPT eliminator +| "eelim" constr_with_bindings_arg OPT eliminator +| "case" induction_clause_list +| "ecase" induction_clause_list +| "fix" ident natural "with" LIST1 fixdecl +| "cofix" ident "with" LIST1 cofixdecl +| "pose" bindings_with_parameters +| "pose" constr as_name +| "epose" bindings_with_parameters +| "epose" constr as_name +| "set" bindings_with_parameters clause_dft_concl +| "set" constr as_name clause_dft_concl +| "eset" bindings_with_parameters clause_dft_concl +| "eset" constr as_name clause_dft_concl +| "remember" constr as_name eqn_ipat clause_dft_all +| "eremember" constr as_name eqn_ipat clause_dft_all +| "assert" test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| "eassert" test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| "assert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "eassert" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "enough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "eenough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic +| "assert" constr as_ipat by_tactic +| "eassert" constr as_ipat by_tactic +| "pose" "proof" lconstr as_ipat +| "epose" "proof" lconstr as_ipat +| "enough" constr as_ipat by_tactic +| "eenough" constr as_ipat by_tactic +| "generalize" constr +| "generalize" constr LIST1 constr +| "generalize" constr lookup_at_as_comma occs as_name LIST0 [ "," pattern_occ as_name ] +| "induction" induction_clause_list +| "einduction" induction_clause_list +| "destruct" induction_clause_list +| "edestruct" induction_clause_list +| "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic +| "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic +| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" constr ] +| "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis "using" constr in_hyp_list +| "red" clause_dft_concl +| "hnf" clause_dft_concl +| "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl +| "cbv" strategy_flag clause_dft_concl +| "cbn" strategy_flag clause_dft_concl +| "lazy" strategy_flag clause_dft_concl +| "compute" delta_flag clause_dft_concl +| "vm_compute" OPT ref_or_pattern_occ clause_dft_concl +| "native_compute" OPT ref_or_pattern_occ clause_dft_concl +| "unfold" LIST1 unfold_occ SEP "," clause_dft_concl +| "fold" LIST1 constr clause_dft_concl +| "pattern" LIST1 pattern_occ SEP "," clause_dft_concl +| "change" conversion clause_dft_concl +| "change_no_check" conversion clause_dft_concl +| "start" "ltac" "profiling" +| "stop" "ltac" "profiling" +| "reset" "ltac" "profile" +| "show" "ltac" "profile" +| "show" "ltac" "profile" "cutoff" int +| "show" "ltac" "profile" string +| "restart_timer" OPT string +| "finish_timing" OPT string +| "finish_timing" "(" string ")" OPT string +| "myred" (* micromega plugin *) +| "psatz_Z" int_or_var tactic (* micromega plugin *) +| "psatz_Z" tactic (* micromega plugin *) +| "xlia" tactic (* micromega plugin *) +| "xnlia" tactic (* micromega plugin *) +| "xnra" tactic (* micromega plugin *) +| "xnqa" tactic (* micromega plugin *) +| "sos_Z" tactic (* micromega plugin *) +| "sos_Q" tactic (* micromega plugin *) +| "sos_R" tactic (* micromega plugin *) +| "lra_Q" tactic (* micromega plugin *) +| "lra_R" tactic (* micromega plugin *) +| "psatz_R" int_or_var tactic (* micromega plugin *) +| "psatz_R" tactic (* micromega plugin *) +| "psatz_Q" int_or_var tactic (* micromega plugin *) +| "psatz_Q" tactic (* micromega plugin *) +| "nsatz_compute" constr (* nsatz plugin *) +| "omega" (* omega plugin *) +| "omega" "with" LIST1 ident (* omega plugin *) +| "omega" "with" "*" (* omega plugin *) +| "rtauto" +| "protect_fv" string "in" ident (* setoid_ring plugin *) +| "protect_fv" string (* setoid_ring plugin *) +| "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* setoid_ring plugin *) +| "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* setoid_ring plugin *) +| "YouShouldNotTypeThis" ssrintrosarg (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +| "YouShouldNotTypeThis" "do" ssrdoarg (* ssr plugin *) +| "YouShouldNotTypeThis" ssrtclarg ssrseqdir ssrseqarg (* ssr plugin *) +| "clear" natural (* ssr plugin *) +| "move" ssrmovearg ssrrpat (* ssr plugin *) +| "move" ssrmovearg ssrclauses (* ssr plugin *) +| "move" ssrrpat (* ssr plugin *) +| "move" (* ssr plugin *) +| "case" ssrcasearg ssrclauses (* ssr plugin *) +| "case" (* ssr plugin *) +| "elim" ssrarg ssrclauses (* ssr plugin *) +| "elim" (* ssr plugin *) +| "apply" ssrapplyarg (* ssr plugin *) +| "apply" (* ssr plugin *) +| "exact" ssrexactarg (* ssr plugin *) +| "exact" (* ssr plugin *) +| "exact" "<:" lconstr (* ssr plugin *) +| "congr" ssrcongrarg (* ssr plugin *) +| "ssrinstancesofruleL2R" ssrterm (* ssr plugin *) +| "ssrinstancesofruleR2L" ssrterm (* ssr plugin *) +| "rewrite" ssrrwargs ssrclauses (* ssr plugin *) +| "unlock" ssrunlockargs ssrclauses (* ssr plugin *) +| "pose" ssrfixfwd (* ssr plugin *) +| "pose" ssrcofixfwd (* ssr plugin *) +| "pose" ssrfwdid ssrposefwd (* ssr plugin *) +| "set" ssrfwdid ssrsetfwd ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| "have" ssrhavefwdwbinders (* ssr plugin *) +| "have" "suff" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "have" "suffices" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suffices" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" ssrsufffwd (* ssr plugin *) +| "suffices" ssrsufffwd (* ssr plugin *) +| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "under" ssrrwarg (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* ssr plugin *) +| "under" ssrrwarg "do" ssrhint3arg (* ssr plugin *) +| "ssrinstancesoftpat" cpattern (* ssrmatching plugin *) +] + +mlname: [ +| preident (* extraction plugin *) +| string (* extraction plugin *) +] + +int_or_id: [ +| preident (* extraction plugin *) +| integer (* extraction plugin *) +] + +language: [ +| "Ocaml" (* extraction plugin *) +| "OCaml" (* extraction plugin *) +| "Haskell" (* extraction plugin *) +| "Scheme" (* extraction plugin *) +| "JSON" (* extraction plugin *) +] + +firstorder_using: [ +| "using" reference +| "using" reference "," LIST1 reference SEP "," +| "using" reference reference LIST0 reference +| +] + +fun_ind_using: [ +| "using" constr_with_bindings (* funind plugin *) +| (* funind plugin *) +] + +with_names: [ +| "as" simple_intropattern (* funind plugin *) +| (* funind plugin *) +] + +constr_comma_sequence': [ +| constr "," constr_comma_sequence' (* funind plugin *) +| constr (* funind plugin *) +] + +auto_using': [ +| "using" constr_comma_sequence' (* funind plugin *) +| (* funind plugin *) +] + +function_rec_definition_loc: [ +| Vernac.rec_definition (* funind plugin *) +] + +fun_scheme_arg: [ +| ident ":=" "Induction" "for" reference "Sort" sort_family (* funind plugin *) +] + +orient: [ +| "->" +| "<-" +| +] + +occurrences: [ +| LIST1 integer +| var +] + +glob: [ +| constr +] + +lglob: [ +| lconstr +] + +casted_constr: [ +| constr +] + +hloc: [ +| +| "in" "|-" "*" +| "in" ident +| "in" "(" "Type" "of" ident ")" +| "in" "(" "Value" "of" ident ")" +| "in" "(" "type" "of" ident ")" +| "in" "(" "value" "of" ident ")" +] + +rename: [ +| ident "into" ident +] + +by_arg_tac: [ +| "by" tactic3 +| +] + +in_clause: [ +| in_clause' +| "*" occs +| "*" "|-" concl_occ +| LIST0 hypident_occ SEP "," "|-" concl_occ +| LIST0 hypident_occ SEP "," +] + +test_lpar_id_colon: [ +| local_test_lpar_id_colon +] + +orient_string: [ +| orient preident +] + +comparison: [ +| "=" +| "<" +| "<=" +| ">" +| ">=" +] + +test: [ +| int_or_var comparison int_or_var +] + +hintbases: [ +| "with" "*" +| "with" LIST1 preident +| +] + +auto_using: [ +| "using" LIST1 uconstr SEP "," +| +] + +hints_path_atom: [ +| LIST1 global +| "_" +] + +hints_path: [ +| "(" hints_path ")" +| hints_path "*" +| "emp" +| "eps" +| hints_path "|" hints_path +| hints_path_atom +| hints_path hints_path +] + +opthints: [ +| ":" LIST1 preident +| +] + +debug: [ +| "debug" +| +] + +eauto_search_strategy: [ +| "(bfs)" +| "(dfs)" +| +] + +tactic_then_last: [ +| "|" LIST0 ( OPT tactic_expr5 ) SEP "|" +| +] + +tactic_then_gen: [ +| tactic_expr5 "|" tactic_then_gen +| tactic_expr5 ".." tactic_then_last +| ".." tactic_then_last +| tactic_expr5 +| "|" tactic_then_gen +| +] + +tactic_then_locality: [ +| "[" OPT ">" +] + +tactic_expr5: [ +| binder_tactic +| tactic_expr4 +] + +tactic_expr4: [ +| tactic_expr3 ";" binder_tactic +| tactic_expr3 ";" tactic_expr3 +| tactic_expr3 ";" tactic_then_locality tactic_then_gen "]" +| tactic_expr3 +| tactic_expr5 ";" "first" ssr_first_else (* ssr plugin *) +| tactic_expr5 ";" "first" ssrseqarg (* ssr plugin *) +| tactic_expr5 ";" "last" ssrseqarg (* ssr plugin *) +] + +tactic_expr3: [ +| "try" tactic_expr3 +| "do" int_or_var tactic_expr3 +| "timeout" int_or_var tactic_expr3 +| "time" OPT string tactic_expr3 +| "repeat" tactic_expr3 +| "progress" tactic_expr3 +| "once" tactic_expr3 +| "exactly_once" tactic_expr3 +| "infoH" tactic_expr3 +| "abstract" tactic_expr2 +| "abstract" tactic_expr2 "using" ident +| selector tactic_expr3 +| tactic_expr2 +| "do" ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "do" ssrortacarg ssrclauses (* ssr plugin *) +| "do" int_or_var ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +] + +tactic_expr2: [ +| tactic_expr1 "+" binder_tactic +| tactic_expr1 "+" tactic_expr2 +| "tryif" tactic_expr5 "then" tactic_expr5 "else" tactic_expr2 +| tactic_expr1 "||" binder_tactic +| tactic_expr1 "||" tactic_expr2 +| tactic_expr1 +] + +tactic_expr1: [ +| match_key "goal" "with" match_context_list "end" +| match_key "reverse" "goal" "with" match_context_list "end" +| match_key tactic_expr5 "with" match_list "end" +| "first" "[" LIST0 tactic_expr5 SEP "|" "]" +| "solve" "[" LIST0 tactic_expr5 SEP "|" "]" +| "idtac" LIST0 message_token +| failkw [ int_or_var | ] LIST0 message_token +| simple_tactic +| tactic_arg +| reference LIST0 tactic_arg_compat +| tactic_expr0 +| tactic_expr5 ssrintros_ne (* ssr plugin *) +] + +tactic_expr0: [ +| "(" tactic_expr5 ")" +| "[" ">" tactic_then_gen "]" +| tactic_atom +| ssrparentacarg (* ssr plugin *) +] + +failkw: [ +| "fail" +| "gfail" +] + +binder_tactic: [ +| "fun" LIST1 input_fun "=>" tactic_expr5 +| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 +| "info" tactic_expr5 +] + +tactic_arg_compat: [ +| tactic_arg +| Constr.constr +| "()" +] + +tactic_arg: [ +| constr_eval +| "fresh" LIST0 fresh_id +| "type_term" uconstr +| "numgoals" +] + +fresh_id: [ +| STRING +| qualid +] + +constr_eval: [ +| "eval" red_expr "in" Constr.constr +| "context" identref "[" Constr.lconstr "]" +| "type" "of" Constr.constr +] + +constr_may_eval: [ +| constr_eval +| Constr.constr +] + +tactic_atom: [ +| integer +| reference +| "()" +] + +match_key: [ +| "match" +| "lazymatch" +| "multimatch" +] + +input_fun: [ +| "_" +| ident +] + +let_clause: [ +| identref ":=" tactic_expr5 +| "_" ":=" tactic_expr5 +| identref LIST1 input_fun ":=" tactic_expr5 +] + +match_pattern: [ +| "context" OPT Constr.ident "[" Constr.lconstr_pattern "]" +| Constr.lconstr_pattern +] + +match_hyps: [ +| name ":" match_pattern +| name ":=" "[" match_pattern "]" ":" match_pattern +| name ":=" match_pattern +] + +match_context_rule: [ +| LIST0 match_hyps SEP "," "|-" match_pattern "=>" tactic_expr5 +| "[" LIST0 match_hyps SEP "," "|-" match_pattern "]" "=>" tactic_expr5 +| "_" "=>" tactic_expr5 +] + +match_context_list: [ +| LIST1 match_context_rule SEP "|" +| "|" LIST1 match_context_rule SEP "|" +] + +match_rule: [ +| match_pattern "=>" tactic_expr5 +| "_" "=>" tactic_expr5 +] + +match_list: [ +| LIST1 match_rule SEP "|" +| "|" LIST1 match_rule SEP "|" +] + +message_token: [ +| identref +| STRING +| integer +] + +ltac_def_kind: [ +| ":=" +| "::=" +] + +tacdef_body: [ +| Constr.global LIST1 input_fun ltac_def_kind tactic_expr5 +| Constr.global ltac_def_kind tactic_expr5 +] + +tactic: [ +| tactic_expr5 +] + +range_selector: [ +| natural "-" natural +| natural +] + +range_selector_or_nth: [ +| natural "-" natural OPT [ "," LIST1 range_selector SEP "," ] +| natural OPT [ "," LIST1 range_selector SEP "," ] +] + +selector_body: [ +| range_selector_or_nth +| test_bracket_ident "[" ident "]" +] + +selector: [ +| "only" selector_body ":" +] + +toplevel_selector: [ +| selector_body ":" +| "!" ":" +| "all" ":" +] + +tactic_mode: [ +| OPT toplevel_selector G_vernac.query_command +| OPT toplevel_selector "{" +| OPT ltac_selector OPT ltac_info tactic ltac_use_default +| "par" ":" OPT ltac_info tactic ltac_use_default +] + +ltac_selector: [ +| toplevel_selector +] + +ltac_info: [ +| "Info" natural +] + +ltac_use_default: [ +| "." +| "..." +] + +ltac_tactic_level: [ +| "(" "at" "level" natural ")" +] + +ltac_production_sep: [ +| "," string +] + +ltac_production_item: [ +| string +| ident "(" ident OPT ltac_production_sep ")" +| ident +] + +ltac_tacdef_body: [ +| tacdef_body +] + +withtac: [ +| "with" Tactic.tactic +| +] + +Constr.closed_binder: [ +| "(" Prim.name ":" Constr.lconstr "|" Constr.lconstr ")" +] + +glob_constr_with_bindings: [ +| constr_with_bindings +] + +rewstrategy: [ +| glob +| "<-" constr +| "subterms" rewstrategy +| "subterm" rewstrategy +| "innermost" rewstrategy +| "outermost" rewstrategy +| "bottomup" rewstrategy +| "topdown" rewstrategy +| "id" +| "fail" +| "refl" +| "progress" rewstrategy +| "try" rewstrategy +| "any" rewstrategy +| "repeat" rewstrategy +| rewstrategy ";" rewstrategy +| "(" rewstrategy ")" +| "choice" rewstrategy rewstrategy +| "old_hints" preident +| "hints" preident +| "terms" LIST0 constr +| "eval" red_expr +| "fold" constr +] + +int_or_var: [ +| integer +| identref +] + +nat_or_var: [ +| natural +| identref +] + +id_or_meta: [ +| identref +] + +open_constr: [ +| constr +] + +uconstr: [ +| constr +] + +destruction_arg: [ +| natural +| test_lpar_id_rpar constr_with_bindings +| constr_with_bindings_arg +] + +constr_with_bindings_arg: [ +| ">" constr_with_bindings +| constr_with_bindings +] + +quantified_hypothesis: [ +| ident +| natural +] + +conversion: [ +| constr +| constr "with" constr +| constr "at" occs_nums "with" constr +] + +occs_nums: [ +| LIST1 nat_or_var +| "-" nat_or_var LIST0 int_or_var +] + +occs: [ +| "at" occs_nums +| +] + +pattern_occ: [ +| constr occs +] + +ref_or_pattern_occ: [ +| smart_global occs +| constr occs +] + +unfold_occ: [ +| smart_global occs +] + +intropatterns: [ +| LIST0 intropattern +] + +ne_intropatterns: [ +| LIST1 intropattern +] + +or_and_intropattern: [ +| "[" LIST1 intropatterns SEP "|" "]" +| "()" +| "(" simple_intropattern ")" +| "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")" +| "(" simple_intropattern "&" LIST1 simple_intropattern SEP "&" ")" +] + +equality_intropattern: [ +| "->" +| "<-" +| "[=" intropatterns "]" +] + +naming_intropattern: [ +| pattern_ident +| "?" +| ident +] + +intropattern: [ +| simple_intropattern +| "*" +| "**" +] + +simple_intropattern: [ +| simple_intropattern_closed LIST0 [ "%" operconstr0 ] +] + +simple_intropattern_closed: [ +| or_and_intropattern +| equality_intropattern +| "_" +| naming_intropattern +] + +simple_binding: [ +| "(" ident ":=" lconstr ")" +| "(" natural ":=" lconstr ")" +] + +bindings: [ +| test_lpar_idnum_coloneq LIST1 simple_binding +| LIST1 constr +] + +constr_with_bindings: [ +| constr with_bindings +] + +with_bindings: [ +| "with" bindings +| +] + +red_flags: [ +| "beta" +| "iota" +| "match" +| "fix" +| "cofix" +| "zeta" +| "delta" delta_flag +] + +delta_flag: [ +| "-" "[" LIST1 smart_global "]" +| "[" LIST1 smart_global "]" +| +] + +strategy_flag: [ +| LIST1 red_flags +| delta_flag +] + +red_expr: [ +| "red" +| "hnf" +| "simpl" delta_flag OPT ref_or_pattern_occ +| "cbv" strategy_flag +| "cbn" strategy_flag +| "lazy" strategy_flag +| "compute" delta_flag +| "vm_compute" OPT ref_or_pattern_occ +| "native_compute" OPT ref_or_pattern_occ +| "unfold" LIST1 unfold_occ SEP "," +| "fold" LIST1 constr +| "pattern" LIST1 pattern_occ SEP "," +| IDENT +] + +hypident: [ +| id_or_meta +| "(" "type" "of" id_or_meta ")" +| "(" "value" "of" id_or_meta ")" +| "(" "type" "of" Prim.identref ")" (* ssr plugin *) +| "(" "value" "of" Prim.identref ")" (* ssr plugin *) +] + +hypident_occ: [ +| hypident occs +] + +clause_dft_concl: [ +| "in" in_clause +| occs +| +] + +clause_dft_all: [ +| "in" in_clause +| +] + +opt_clause: [ +| "in" in_clause +| "at" occs_nums +| +] + +concl_occ: [ +| "*" occs +| +] + +in_hyp_list: [ +| "in" LIST1 id_or_meta +| +] + +in_hyp_as: [ +| "in" id_or_meta as_ipat +| +] + +simple_binder: [ +| name +| "(" LIST1 name ":" lconstr ")" +] + +fixdecl: [ +| "(" ident LIST0 simple_binder fixannot ":" lconstr ")" +] + +cofixdecl: [ +| "(" ident LIST0 simple_binder ":" lconstr ")" +] + +bindings_with_parameters: [ +| check_for_coloneq "(" ident LIST0 simple_binder ":=" lconstr ")" +] + +eliminator: [ +| "using" constr_with_bindings +] + +as_ipat: [ +| "as" simple_intropattern +| +] + +or_and_intropattern_loc: [ +| or_and_intropattern +| identref +] + +as_or_and_ipat: [ +| "as" or_and_intropattern_loc +| +] + +eqn_ipat: [ +| "eqn" ":" naming_intropattern +| "_eqn" ":" naming_intropattern +| "_eqn" +| +] + +as_name: [ +| "as" ident +| +] + +by_tactic: [ +| "by" tactic_expr3 +| +] + +rewriter: [ +| "!" constr_with_bindings_arg +| [ "?" | LEFTQMARK ] constr_with_bindings_arg +| natural "!" constr_with_bindings_arg +| natural [ "?" | LEFTQMARK ] constr_with_bindings_arg +| natural constr_with_bindings_arg +| constr_with_bindings_arg +] + +oriented_rewriter: [ +| orient rewriter +] + +induction_clause: [ +| destruction_arg as_or_and_ipat eqn_ipat opt_clause +] + +induction_clause_list: [ +| LIST1 induction_clause SEP "," OPT eliminator opt_clause +] + +ring_mod: [ +| "decidable" constr (* setoid_ring plugin *) +| "abstract" (* setoid_ring plugin *) +| "morphism" constr (* setoid_ring plugin *) +| "constants" "[" tactic "]" (* setoid_ring plugin *) +| "closed" "[" LIST1 global "]" (* setoid_ring plugin *) +| "preprocess" "[" tactic "]" (* setoid_ring plugin *) +| "postprocess" "[" tactic "]" (* setoid_ring plugin *) +| "setoid" constr constr (* setoid_ring plugin *) +| "sign" constr (* setoid_ring plugin *) +| "power" constr "[" LIST1 global "]" (* setoid_ring plugin *) +| "power_tac" constr "[" tactic "]" (* setoid_ring plugin *) +| "div" constr (* setoid_ring plugin *) +] + +ring_mods: [ +| "(" LIST1 ring_mod SEP "," ")" (* setoid_ring plugin *) +] + +field_mod: [ +| ring_mod (* setoid_ring plugin *) +| "completeness" constr (* setoid_ring plugin *) +] + +field_mods: [ +| "(" LIST1 field_mod SEP "," ")" (* setoid_ring plugin *) +] + +ssrtacarg: [ +| tactic_expr5 (* ssr plugin *) +] + +ssrtac3arg: [ +| tactic_expr3 (* ssr plugin *) +] + +ssrtclarg: [ +| ssrtacarg (* ssr plugin *) +] + +ssrhyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_hyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_id: [ +| ident (* ssr plugin *) +] + +ssrsimpl_ne: [ +| "//=" (* ssr plugin *) +| "/=" (* ssr plugin *) +| test_ssrslashnum11 "/" natural "/" natural "=" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "/" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "=" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "/=" (* ssr plugin *) +| test_ssrslashnum10 "/" natural "/" "=" (* ssr plugin *) +| test_ssrslashnum01 "//" natural "=" (* ssr plugin *) +| test_ssrslashnum00 "//" (* ssr plugin *) +] + +ssrclear_ne: [ +| "{" LIST1 ssrhyp "}" (* ssr plugin *) +] + +ssrclear: [ +| ssrclear_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrindex: [ +| int_or_var (* ssr plugin *) +] + +ssrocc: [ +| natural LIST0 natural (* ssr plugin *) +| "-" LIST0 natural (* ssr plugin *) +| "+" LIST0 natural (* ssr plugin *) +] + +ssrmmod: [ +| "!" (* ssr plugin *) +| LEFTQMARK (* ssr plugin *) +| "?" (* ssr plugin *) +] + +ssrmult_ne: [ +| natural ssrmmod (* ssr plugin *) +| ssrmmod (* ssr plugin *) +] + +ssrmult: [ +| ssrmult_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrdocc: [ +| "{" ssrocc "}" (* ssr plugin *) +| "{" LIST0 ssrhyp "}" (* ssr plugin *) +] + +ssrterm: [ +| "YouShouldNotTypeThis" constr (* ssr plugin *) +| ssrtermkind Pcoq.Constr.constr (* ssr plugin *) +] + +ast_closure_term: [ +| term_annotation constr (* ssr plugin *) +] + +ast_closure_lterm: [ +| term_annotation lconstr (* ssr plugin *) +] + +ssrbwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| test_not_ssrslashnum "/" Pcoq.Constr.constr (* ssr plugin *) +| test_not_ssrslashnum "/" Pcoq.Constr.constr ssrbwdview (* ssr plugin *) +] + +ssrfwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| test_not_ssrslashnum "/" ast_closure_term (* ssr plugin *) +| test_not_ssrslashnum "/" ast_closure_term ssrfwdview (* ssr plugin *) +] + +ident_no_do: [ +| "YouShouldNotTypeThis" ident (* ssr plugin *) +| test_ident_no_do IDENT (* ssr plugin *) +] + +ssripat: [ +| "_" (* ssr plugin *) +| "*" (* ssr plugin *) +| ">" (* ssr plugin *) +| ident_no_do (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| "++" (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| ssrdocc (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +| "-" (* ssr plugin *) +| "-/" "=" (* ssr plugin *) +| "-/=" (* ssr plugin *) +| "-/" "/" (* ssr plugin *) +| "-//" (* ssr plugin *) +| "-/" integer "/" (* ssr plugin *) +| "-/" "/=" (* ssr plugin *) +| "-//" "=" (* ssr plugin *) +| "-//=" (* ssr plugin *) +| "-/" integer "/=" (* ssr plugin *) +| "-/" integer "/" integer "=" (* ssr plugin *) +| ssrfwdview (* ssr plugin *) +| "[" ":" LIST0 ident "]" (* ssr plugin *) +| "[:" LIST0 ident "]" (* ssr plugin *) +| ssrcpat (* ssr plugin *) +] + +ssripats: [ +| ssripat ssripats (* ssr plugin *) +| (* ssr plugin *) +] + +ssriorpat: [ +| ssripats "|" ssriorpat (* ssr plugin *) +| ssripats "|-" ">" ssriorpat (* ssr plugin *) +| ssripats "|-" ssriorpat (* ssr plugin *) +| ssripats "|->" ssriorpat (* ssr plugin *) +| ssripats "||" ssriorpat (* ssr plugin *) +| ssripats "|||" ssriorpat (* ssr plugin *) +| ssripats "||||" ssriorpat (* ssr plugin *) +| ssripats (* ssr plugin *) +] + +ssrcpat: [ +| "YouShouldNotTypeThis" ssriorpat (* ssr plugin *) +| test_nohidden "[" hat "]" (* ssr plugin *) +| test_nohidden "[" ssriorpat "]" (* ssr plugin *) +| test_nohidden "[=" ssriorpat "]" (* ssr plugin *) +] + +hat: [ +| "^" ident (* ssr plugin *) +| "^" "~" ident (* ssr plugin *) +| "^" "~" natural (* ssr plugin *) +| "^~" ident (* ssr plugin *) +| "^~" natural (* ssr plugin *) +] + +ssripats_ne: [ +| ssripat ssripats (* ssr plugin *) +] + +ssrhpats: [ +| ssripats (* ssr plugin *) +] + +ssrhpats_wtransp: [ +| ssripats (* ssr plugin *) +| ssripats "@" ssripats (* ssr plugin *) +] + +ssrhpats_nobs: [ +| ssripats (* ssr plugin *) +] + +ssrrpat: [ +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrintros_ne: [ +| "=>" ssripats_ne (* ssr plugin *) +] + +ssrintros: [ +| ssrintros_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrintrosarg: [ +| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne (* ssr plugin *) +] + +ssrfwdid: [ +| test_ssrfwdid Prim.ident (* ssr plugin *) +] + +ssrortacs: [ +| ssrtacarg "|" ssrortacs (* ssr plugin *) +| ssrtacarg "|" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +| "|" ssrortacs (* ssr plugin *) +| "|" (* ssr plugin *) +] + +ssrhintarg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +] + +ssrhint3arg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtac3arg (* ssr plugin *) +] + +ssrortacarg: [ +| "[" ssrortacs "]" (* ssr plugin *) +] + +ssrhint: [ +| (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +] + +ssrwgen: [ +| ssrclear_ne (* ssr plugin *) +| ssrhoi_hyp (* ssr plugin *) +| "@" ssrhoi_hyp (* ssr plugin *) +| "(" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" ssrhoi_id ")" (* ssr plugin *) +| "(@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" "@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +] + +ssrclausehyps: [ +| ssrwgen "," ssrclausehyps (* ssr plugin *) +| ssrwgen ssrclausehyps (* ssr plugin *) +| ssrwgen (* ssr plugin *) +] + +ssrclauses: [ +| "in" ssrclausehyps "|-" "*" (* ssr plugin *) +| "in" ssrclausehyps "|-" (* ssr plugin *) +| "in" ssrclausehyps "*" (* ssr plugin *) +| "in" ssrclausehyps (* ssr plugin *) +| "in" "|-" "*" (* ssr plugin *) +| "in" "*" (* ssr plugin *) +| "in" "*" "|-" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrfwd: [ +| ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrbvar: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +] + +ssrbinder: [ +| ssrbvar (* ssr plugin *) +| "(" ssrbvar ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar LIST1 ssrbvar ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ":=" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":=" lconstr ")" (* ssr plugin *) +| [ "of" | "&" ] operconstr99 (* ssr plugin *) +] + +ssrstruct: [ +| "{" "struct" ident "}" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrposefwd: [ +| LIST0 ssrbinder ssrfwd (* ssr plugin *) +] + +ssrfixfwd: [ +| "fix" ssrbvar LIST0 ssrbinder ssrstruct ssrfwd (* ssr plugin *) +] + +ssrcofixfwd: [ +| "cofix" ssrbvar LIST0 ssrbinder ssrfwd (* ssr plugin *) +] + +ssrsetfwd: [ +| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":" ast_closure_lterm ":=" lcpattern (* ssr plugin *) +| ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":=" lcpattern (* ssr plugin *) +] + +ssrhavefwd: [ +| ":" ast_closure_lterm ssrhint (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" (* ssr plugin *) +| ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrhavefwdwbinders: [ +| ssrhpats_wtransp LIST0 ssrbinder ssrhavefwd (* ssr plugin *) +] + +ssrdoarg: [ +] + +ssrseqarg: [ +| ssrswap (* ssr plugin *) +| ssrseqidx ssrortacarg OPT ssrorelse (* ssr plugin *) +| ssrseqidx ssrswap (* ssr plugin *) +| tactic_expr3 (* ssr plugin *) +] + +ssrseqidx: [ +| test_ssrseqvar Prim.ident (* ssr plugin *) +| Prim.natural (* ssr plugin *) +] + +ssrswap: [ +| "first" (* ssr plugin *) +| "last" (* ssr plugin *) +] + +ssrorelse: [ +| "||" tactic_expr2 (* ssr plugin *) +] + +Prim.ident: [ +| IDENT ssr_null_entry (* ssr plugin *) +] + +ssrparentacarg: [ +| "(" tactic_expr5 ")" (* ssr plugin *) +] + +ssrdotac: [ +| tactic_expr3 (* ssr plugin *) +| ssrortacarg (* ssr plugin *) +] + +ssrseqdir: [ +] + +ssr_first: [ +| ssr_first ssrintros_ne (* ssr plugin *) +| "[" LIST0 tactic_expr5 SEP "|" "]" (* ssr plugin *) +] + +ssr_first_else: [ +| ssr_first ssrorelse (* ssr plugin *) +| ssr_first (* ssr plugin *) +] + +ssrgen: [ +| ssrdocc cpattern (* ssr plugin *) +| cpattern (* ssr plugin *) +] + +ssrdgens_tl: [ +| "{" LIST1 ssrhyp "}" cpattern ssrdgens_tl (* ssr plugin *) +| "{" LIST1 ssrhyp "}" (* ssr plugin *) +| "{" ssrocc "}" cpattern ssrdgens_tl (* ssr plugin *) +| "/" ssrdgens_tl (* ssr plugin *) +| cpattern ssrdgens_tl (* ssr plugin *) +| (* ssr plugin *) +] + +ssrdgens: [ +| ":" ssrgen ssrdgens_tl (* ssr plugin *) +] + +ssreqid: [ +| test_ssreqid ssreqpat (* ssr plugin *) +| test_ssreqid (* ssr plugin *) +] + +ssreqpat: [ +| Prim.ident (* ssr plugin *) +| "_" (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrarg: [ +| ssrfwdview ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrfwdview ssrclear ssrintros (* ssr plugin *) +| ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +] + +ssrmovearg: [ +| ssrarg (* ssr plugin *) +] + +ssrcasearg: [ +| ssrarg (* ssr plugin *) +] + +ssragen: [ +| "{" LIST1 ssrhyp "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssragens: [ +| "{" LIST1 ssrhyp "}" ssrterm ssragens (* ssr plugin *) +| "{" LIST1 ssrhyp "}" (* ssr plugin *) +| ssrterm ssragens (* ssr plugin *) +| (* ssr plugin *) +] + +ssrapplyarg: [ +| ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +| ssrbwdview ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrbwdview ssrclear ssrintros (* ssr plugin *) +] + +ssrexactarg: [ +| ":" ssragen ssragens (* ssr plugin *) +| ssrbwdview ssrclear (* ssr plugin *) +| ssrclear_ne (* ssr plugin *) +] + +ssrcongrarg: [ +| natural constr ssrdgens (* ssr plugin *) +| natural constr (* ssr plugin *) +| constr ssrdgens (* ssr plugin *) +| constr (* ssr plugin *) +] + +ssrrwocc: [ +| "{" LIST0 ssrhyp "}" (* ssr plugin *) +| "{" ssrocc "}" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrrule_ne: [ +| test_not_ssrslashnum [ "/" ssrterm | ssrterm | ssrsimpl_ne ] (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +] + +ssrrule: [ +| ssrrule_ne (* ssr plugin *) +| (* ssr plugin *) +] + +ssrpattern_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrpattern_ne_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +] + +ssrrwarg: [ +| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "-/" ssrterm (* ssr plugin *) +| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" LIST1 ssrhyp "}" ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| "{" LIST1 ssrhyp "}" ssrrule (* ssr plugin *) +| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| ssrrule_ne (* ssr plugin *) +] + +ssrrwargs: [ +| test_ssr_rw_syntax LIST1 ssrrwarg (* ssr plugin *) +] + +ssrunlockarg: [ +| "{" ssrocc "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrunlockargs: [ +| LIST0 ssrunlockarg (* ssr plugin *) +] + +ssrsufffwd: [ +| ssrhpats LIST0 ssrbinder ":" ast_closure_lterm ssrhint (* ssr plugin *) +] + +ssrwlogfwd: [ +| ":" LIST0 ssrwgen "/" ast_closure_lterm (* ssr plugin *) +] + +ssr_idcomma: [ +| (* ssr plugin *) +| test_idcomma [ IDENT | "_" ] "," (* ssr plugin *) +] + +ssr_rtype: [ +| "return" operconstr100 (* ssr plugin *) +] + +ssr_mpat: [ +| pattern200 (* ssr plugin *) +] + +ssr_dpat: [ +| ssr_mpat "in" pattern200 ssr_rtype (* ssr plugin *) +| ssr_mpat ssr_rtype (* ssr plugin *) +| ssr_mpat (* ssr plugin *) +] + +ssr_dthen: [ +| ssr_dpat "then" lconstr (* ssr plugin *) +] + +ssr_elsepat: [ +| "else" (* ssr plugin *) +] + +ssr_else: [ +| ssr_elsepat lconstr (* ssr plugin *) +] + +ssr_search_item: [ +| string (* ssr plugin *) +| string "%" preident (* ssr plugin *) +| constr_pattern (* ssr plugin *) +] + +ssr_search_arg: [ +| "-" ssr_search_item ssr_search_arg (* ssr plugin *) +| ssr_search_item ssr_search_arg (* ssr plugin *) +| (* ssr plugin *) +] + +ssr_modlocs: [ +| (* ssr plugin *) +| "in" LIST1 modloc (* ssr plugin *) +] + +modloc: [ +| "-" global (* ssr plugin *) +| global (* ssr plugin *) +] + +ssrhintref: [ +| constr (* ssr plugin *) +| constr "|" natural (* ssr plugin *) +] + +ssrviewpos: [ +| "for" "move" "/" (* ssr plugin *) +| "for" "apply" "/" (* ssr plugin *) +| "for" "apply" "/" "/" (* ssr plugin *) +| "for" "apply" "//" (* ssr plugin *) +| (* ssr plugin *) +] + +ssrviewposspc: [ +| ssrviewpos (* ssr plugin *) +] + +rpattern: [ +| lconstr (* ssrmatching plugin *) +| "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr (* ssrmatching plugin *) +| "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "as" lconstr "in" lconstr (* ssrmatching plugin *) +] + +cpattern: [ +| "Qed" constr (* ssrmatching plugin *) +| ssrtermkind constr (* ssrmatching plugin *) +] + +lcpattern: [ +| "Qed" lconstr (* ssrmatching plugin *) +| ssrtermkind lconstr (* ssrmatching plugin *) +] + +ssrpatternarg: [ +| rpattern (* ssrmatching plugin *) +] + +numnotoption: [ +| +| "(" "warning" "after" bigint ")" +| "(" "abstract" "after" bigint ")" +] + diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar new file mode 100644 index 0000000000..cd6e11505c --- /dev/null +++ b/doc/tools/docgram/orderedGrammar @@ -0,0 +1,4170 @@ +(* Defines the order to apply to editedGrammar to get productionlistGrammar. +doc_grammar will modify this file to add/remove nonterminals and productions +to match editedGrammar, which will remove comments. Not compiled into Coq *) +DOC_GRAMMAR + +global: [ +| reference +] + +constr_pattern: [ +| term +] + +sort: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +| "Type" "@{" "_" "}" +| "Type" "@{" universe "}" +] + +sort_family: [ +| "Set" +| "Prop" +| "SProp" +| "Type" +] + +universe_increment: [ +| "+" natural +| empty +] + +universe_name: [ +| global +| "Set" +| "Prop" +] + +universe_expr: [ +| universe_name universe_increment +] + +universe: [ +| "max" "(" universe_expr_list_comma ")" +| universe_expr +] + +universe_expr_list_comma: [ +| universe_expr_list_comma "," universe_expr +| universe_expr +] + +lconstr: [ +| operconstr200 +| lconstr +] + +term: [ +| operconstr8 +| "@" global instance +] + +operconstr200: [ +| binder_constr +| operconstr100 +] + +operconstr100: [ +| operconstr99 "<:" binder_constr +| operconstr99 "<:" operconstr100 +| operconstr99 "<<:" binder_constr +| operconstr99 "<<:" operconstr100 +| operconstr99 ":" binder_constr +| operconstr99 ":" operconstr100 +| operconstr99 ":>" +| operconstr99 +] + +operconstr99: [ +| operconstr90 +] + +operconstr90: [ +| operconstr10 +] + +operconstr10: [ +| operconstr9 appl_arg_list +| "@" global instance operconstr9_list_opt +| "@" pattern_identref ident_list +| operconstr9 +] + +appl_arg_list: [ +| appl_arg_list appl_arg +| appl_arg +] + +operconstr9: [ +| ".." operconstr0 ".." +| operconstr8 +] + +operconstr8: [ +| operconstr1 +] + +operconstr1: [ +| operconstr0 ".(" global appl_arg_list_opt ")" +| operconstr0 ".(" "@" global operconstr9_list_opt ")" +| operconstr0 "%" IDENT +| operconstr0 +] + +appl_arg_list_opt: [ +| appl_arg_list_opt appl_arg +| empty +] + +operconstr9_list_opt: [ +| operconstr9_list_opt operconstr9 +| empty +] + +operconstr0: [ +| atomic_constr +| match_constr +| "(" operconstr200 ")" +| "{|" record_declaration bar_cbrace +| "{" binder_constr "}" +| "`{" operconstr200 "}" +| "`(" operconstr200 ")" +| "ltac" ":" "(" ltac_expr ")" +] + +record_declaration: [ +| record_fields +] + +record_fields: [ +| record_field_declaration ";" record_fields +| record_field_declaration +| empty +| record_field ";" record_fields +| record_field ";" +| record_field +] + +record_field_declaration: [ +| global binders ":=" lconstr +] + +binder_constr: [ +| "forall" open_binders "," operconstr200 +| "fun" open_binders "=>" operconstr200 +| "let" name binders type_cstr ":=" operconstr200 "in" operconstr200 +| "let" single_fix "in" operconstr200 +| "let" name_alt return_type ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 "in" operconstr200 +| "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200 +| "if" operconstr200 return_type "then" operconstr200 "else" operconstr200 +| fix_constr +| "if" operconstr200 "is" ssr_dthen ssr_else (* ssr plugin *) +| "if" operconstr200 "isn't" ssr_dthen ssr_else (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +| "let" ":" ssr_mpat "in" pattern200 ":=" lconstr ssr_rtype "in" lconstr (* ssr plugin *) +] + +name_alt: [ +| "(" name_list_comma_opt ")" +| "()" +] + +name_list_comma_opt: [ +| name_list_comma +| empty +] + +name_list_comma: [ +| name_list_comma "," name +| name +] + +name_list_opt: [ +| name_list_opt name +| empty +] + +name_list: [ +| name_list name +| name +] + +appl_arg: [ +| lpar_id_coloneq lconstr ")" +| operconstr9 +] + +atomic_constr: [ +| global instance +| sort +| NUMERAL +| string +| "_" +| "?" "[" ident "]" +| "?" "[" "?" ident "]" +| "?" ident evar_instance +] + +inst: [ +| ident ":=" lconstr +] + +evar_instance: [ +| "@{" inst_list_semi "}" +| empty +] + +inst_list_semi: [ +| inst_list_semi ";" inst +| inst +] + +instance: [ +| "@{" universe_level_list_opt "}" +| empty +] + +universe_level_list_opt: [ +| universe_level_list_opt universe_level +| empty +] + +universe_level: [ +| "Set" +| "Prop" +| "Type" +| "_" +| global +] + +fix_constr: [ +| single_fix +| single_fix "with" fix_decl_list "for" ident +] + +fix_decl_list: [ +| fix_decl_list "with" fix_decl +| fix_decl +] + +single_fix: [ +| fix_kw fix_decl +] + +fix_kw: [ +| "fix" +| "cofix" +] + +fix_decl: [ +| ident binders_fixannot type_cstr ":=" operconstr200 +] + +match_constr: [ +| "match" case_item_list_comma case_type_opt "with" branches "end" +] + +case_item_list_comma: [ +| case_item_list_comma "," case_item +| case_item +] + +case_type_opt: [ +| case_type +| empty +] + +case_item: [ +| operconstr100 as_opt in_opt +] + +as_opt2: [ +| as_opt case_type +| empty +] + +in_opt: [ +| "in" pattern200 +| empty +] + +case_type: [ +| "return" operconstr100 +] + +return_type: [ +| as_opt2 +] + +as_opt3: [ +| "as" dirpath +| empty +] + +branches: [ +| or_opt eqn_list_or_opt +] + +mult_pattern: [ +| pattern200_list_comma +] + +pattern200_list_comma: [ +| pattern200_list_comma "," pattern200 +| pattern200 +] + +eqn: [ +| mult_pattern_list_or "=>" lconstr +] + +mult_pattern_list_or: [ +| mult_pattern_list_or "|" mult_pattern +| mult_pattern +] + +record_pattern: [ +| global ":=" pattern200 +] + +record_patterns: [ +| record_pattern ";" record_patterns +| record_pattern ";" +| record_pattern +| empty +] + +pattern200: [ +| pattern100 +] + +pattern100: [ +| pattern99 ":" binder_constr +| pattern99 ":" operconstr100 +| pattern99 +] + +pattern99: [ +| pattern90 +] + +pattern90: [ +| pattern10 +] + +pattern10: [ +| pattern1 "as" name +| pattern1 pattern1_list +| "@" reference pattern1_list_opt +| pattern1 +] + +pattern1_list: [ +| pattern1_list pattern1 +| pattern1 +] + +pattern1_list_opt: [ +| pattern1_list_opt pattern1 +| empty +] + +pattern1: [ +| pattern0 "%" IDENT +| pattern0 +] + +pattern0: [ +| reference +| "{|" record_patterns bar_cbrace +| "_" +| "(" pattern200 ")" +| "(" pattern200 "|" pattern200_list_or ")" +| NUMERAL +| string +] + +pattern200_list_or: [ +| pattern200_list_or "|" pattern200 +| pattern200 +] + +impl_ident_tail: [ +| "}" +| name_list ":" lconstr "}" +| name_list "}" +| ":" lconstr "}" +] + +fixannot: [ +| "{" "struct" ident "}" +| "{" "wf" term ident "}" +| "{" "measure" term ident_opt term_opt "}" +| "{" "struct" name "}" +| empty +] + +term_opt: [ +| term +| empty +] + +impl_name_head: [ +| empty +] + +binders_fixannot: [ +| impl_name_head impl_ident_tail binders_fixannot +| fixannot +| binder binders_fixannot +| empty +] + +open_binders: [ +| name name_list_opt ":" lconstr +| name name_list_opt binders +| name ".." name +| closed_binder binders +] + +binders: [ +| binder_list_opt +] + +binder_list_opt: [ +| binder_list_opt binder +| empty +] + +binder: [ +| name +| closed_binder +] + +typeclass_constraint: [ +| "!" operconstr200 +| "{" name "}" ":" exclam_opt operconstr200 +| name_colon exclam_opt operconstr200 +| operconstr200 +] + +type_cstr: [ +| lconstr_opt +| ":" lconstr +| empty +] + +preident: [ +| IDENT +] + +pattern_identref: [ +| "?" ident +] + +var: [ +| ident +] + +field: [ +| FIELD +] + +fields: [ +| field fields +| field +] + +fullyqualid: [ +| ident fields +| ident +] + +basequalid: [ +| ident fields +| ident +] + +name: [ +| "_" +| ident +] + +reference: [ +| ident fields +| ident +] + +by_notation: [ +| ne_string IDENT_opt +] + +IDENT_opt: [ +| "%" IDENT +| empty +] + +smart_global: [ +| reference +| by_notation +] + +qualid: [ +| basequalid +] + +ne_string: [ +| STRING +] + +ne_lstring: [ +| ne_string +] + +dirpath: [ +| ident field_list_opt +] + +field_list_opt: [ +| field_list_opt field +| empty +] + +string: [ +| STRING +] + +lstring: [ +| string +] + +integer: [ +| NUMERAL +| "-" NUMERAL +] + +natural: [ +| NUMERAL +] + +bigint: [ +| NUMERAL +] + +bar_cbrace: [ +| "|" "}" +] + +vernac_control: [ +| "Time" vernac_control +| "Redirect" ne_string vernac_control +| "Timeout" natural vernac_control +| "Fail" vernac_control +| decorated_vernac +] + +decorated_vernac: [ +| quoted_attributes_list_opt vernac +] + +quoted_attributes_list_opt: [ +| quoted_attributes_list_opt quoted_attributes +| empty +] + +quoted_attributes: [ +| "#[" attribute_list_comma_opt "]" +] + +attribute_list_comma_opt: [ +| attribute_list_comma +| empty +] + +attribute_list_comma: [ +| attribute_list_comma "," attribute +| attribute +] + +attribute: [ +| ident attribute_value +] + +attribute_value: [ +| "=" string +| "(" attribute_list_comma_opt ")" +| empty +] + +vernac: [ +| "Local" vernac_poly +| "Global" vernac_poly +| vernac_poly +] + +vernac_poly: [ +| "Polymorphic" vernac_aux +| "Monomorphic" vernac_aux +| vernac_aux +] + +vernac_aux: [ +| "Program" gallina "." +| "Program" gallina_ext "." +| gallina "." +| gallina_ext "." +| command "." +| syntax "." +| subprf +| command_entry +] + +noedit_mode: [ +| query_command +] + +subprf: [ +| BULLET +| "{" +| "}" +] + +gallina: [ +| thm_token ident_decl binders ":" lconstr with_list_opt +| assumption_token inline assum_list +| assumptions_token inline assum_list +| def_token ident_decl def_body +| "Let" ident def_body +| cumulativity_token_opt private_token finite_token inductive_definition_list +| "Fixpoint" rec_definition_list +| "Let" "Fixpoint" rec_definition_list +| "CoFixpoint" corec_definition_list +| "Let" "CoFixpoint" corec_definition_list +| "Scheme" scheme_list +| "Combined" "Scheme" ident "from" ident_list_comma +| "Register" global "as" qualid +| "Register" "Inline" global +| "Primitive" ident lconstr_opt ":=" register_token +| "Universe" ident_list +| "Universes" ident_list +| "Constraint" univ_constraint_list_comma +] + +with_list_opt: [ +| with_list_opt "with" ident_decl binders ":" lconstr +| empty +] + +cumulativity_token_opt: [ +| cumulativity_token +| empty +] + +inductive_definition_list: [ +| inductive_definition_list "with" inductive_definition +| inductive_definition +] + +rec_definition_list: [ +| rec_definition_list "with" rec_definition +| rec_definition +] + +corec_definition_list: [ +| corec_definition_list "with" corec_definition +| corec_definition +] + +scheme_list: [ +| scheme_list "with" scheme +| scheme +] + +ident_list_comma: [ +| ident_list_comma "," ident +| ident +] + +univ_constraint_list_comma: [ +| univ_constraint_list_comma "," univ_constraint +| univ_constraint +] + +lconstr_opt2: [ +| ":=" lconstr +| empty +] + +register_token: [ +| register_prim_token +| register_type_token +] + +register_type_token: [ +| "#int63_type" +] + +register_prim_token: [ +| "#int63_head0" +| "#int63_tail0" +| "#int63_add" +| "#int63_sub" +| "#int63_mul" +| "#int63_div" +| "#int63_mod" +| "#int63_lsr" +| "#int63_lsl" +| "#int63_land" +| "#int63_lor" +| "#int63_lxor" +| "#int63_addc" +| "#int63_subc" +| "#int63_addcarryc" +| "#int63_subcarryc" +| "#int63_mulc" +| "#int63_diveucl" +| "#int63_div21" +| "#int63_addmuldiv" +| "#int63_eq" +| "#int63_lt" +| "#int63_le" +| "#int63_compare" +] + +thm_token: [ +| "Theorem" +| "Lemma" +| "Fact" +| "Remark" +| "Corollary" +| "Proposition" +| "Property" +] + +def_token: [ +| "Definition" +| "Example" +| "SubClass" +] + +assumption_token: [ +| "Hypothesis" +| "Variable" +| "Axiom" +| "Parameter" +| "Conjecture" +] + +assumptions_token: [ +| "Hypotheses" +| "Variables" +| "Axioms" +| "Parameters" +| "Conjectures" +] + +inline: [ +| "Inline" "(" natural ")" +| "Inline" +| empty +] + +univ_constraint: [ +| universe_name lt_alt universe_name +] + +lt_alt: [ +| "<" +| "=" +| "<=" +] + +univ_decl: [ +| "@{" ident_list_opt plus_opt univ_constraint_alt +] + +plus_opt: [ +| "+" +| empty +] + +univ_constraint_alt: [ +| "|" univ_constraint_list_comma_opt plus_opt "}" +| rbrace_alt +] + +univ_constraint_list_comma_opt: [ +| univ_constraint_list_comma +| empty +] + +rbrace_alt: [ +| "}" +| bar_cbrace +] + +ident_decl: [ +| ident univ_decl_opt +] + +finite_token: [ +| "Inductive" +| "CoInductive" +| "Variant" +| "Record" +| "Structure" +| "Class" +] + +cumulativity_token: [ +| "Cumulative" +| "NonCumulative" +] + +private_token: [ +| "Private" +| empty +] + +def_body: [ +| binders ":=" reduce lconstr +| binders ":" lconstr ":=" reduce lconstr +| binders ":" lconstr +] + +reduce: [ +| "Eval" red_expr "in" +| empty +] + +one_decl_notation: [ +| ne_lstring ":=" term IDENT_opt2 +] + +IDENT_opt2: [ +| ":" IDENT +| empty +] + +decl_sep: [ +| "and" +] + +decl_notation: [ +| "where" one_decl_notation_list +| empty +] + +one_decl_notation_list: [ +| one_decl_notation_list decl_sep one_decl_notation +| one_decl_notation +] + +opt_constructors_or_fields: [ +| ":=" constructor_list_or_record_decl +| empty +] + +inductive_definition: [ +| opt_coercion ident_decl binders lconstr_opt opt_constructors_or_fields decl_notation +] + +constructor_list_or_record_decl: [ +| "|" constructor_list_or +| ident constructor_type "|" constructor_list_or_opt +| ident constructor_type +| ident "{" record_fields "}" +| "{" record_fields "}" +| empty +] + +constructor_list_or: [ +| constructor_list_or "|" constructor +| constructor +] + +constructor_list_or_opt: [ +| constructor_list_or +| empty +] + +opt_coercion: [ +| ">" +| empty +] + +rec_definition: [ +| ident_decl binders_fixannot type_cstr lconstr_opt2 decl_notation +] + +corec_definition: [ +| ident_decl binders type_cstr lconstr_opt2 decl_notation +] + +lconstr_opt: [ +| ":" lconstr +| empty +] + +scheme: [ +| scheme_kind +| ident ":=" scheme_kind +] + +scheme_kind: [ +| "Induction" "for" smart_global "Sort" sort_family +| "Minimality" "for" smart_global "Sort" sort_family +| "Elimination" "for" smart_global "Sort" sort_family +| "Case" "for" smart_global "Sort" sort_family +| "Equality" "for" smart_global +] + +record_field: [ +| quoted_attributes_list_opt record_binder natural_opt2 decl_notation +] + +record_binder_body: [ +| binders of_type_with_opt_coercion lconstr +| binders of_type_with_opt_coercion lconstr ":=" lconstr +| binders ":=" lconstr +] + +record_binder: [ +| name +| name record_binder_body +] + +assum_list: [ +| assum_coe_list +| simple_assum_coe +] + +assum_coe_list: [ +| assum_coe_list assum_coe +| assum_coe +] + +assum_coe: [ +| "(" simple_assum_coe ")" +] + +simple_assum_coe: [ +| ident_decl_list of_type_with_opt_coercion lconstr +] + +ident_decl_list: [ +| ident_decl_list ident_decl +| ident_decl +] + +constructor_type: [ +| binders of_type_with_opt_coercion_opt +] + +of_type_with_opt_coercion_opt: [ +| of_type_with_opt_coercion lconstr +| empty +] + +constructor: [ +| ident constructor_type +] + +of_type_with_opt_coercion: [ +| ":>>" +| ":>" ">" +| ":>" +| ":" ">" ">" +| ":" ">" +| ":" +] + +gallina_ext: [ +| "Module" export_token ident module_binder_list_opt of_module_type is_module_expr +| "Module" "Type" ident module_binder_list_opt check_module_types is_module_type +| "Declare" "Module" export_token ident module_binder_list_opt ":" module_type_inl +| "Section" ident +| "Chapter" ident +| "End" ident +| "Collection" ident ":=" section_subset_expr +| "Require" export_token global_list +| "From" global "Require" export_token global_list +| "Import" global_list +| "Export" global_list +| "Include" module_type_inl ext_module_expr_list_opt +| "Include" "Type" module_type_inl ext_module_type_list_opt +| "Transparent" smart_global_list +| "Opaque" smart_global_list +| "Strategy" strategy_level_list +| "Canonical" Structure_opt global univ_decl_opt2 +| "Canonical" Structure_opt by_notation +| "Coercion" global univ_decl_opt def_body +| "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr +| "Coercion" global ":" class_rawexpr ">->" class_rawexpr +| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr +| "Context" binder_list +| "Instance" instance_name ":" operconstr200 hint_info record_declaration_opt +| "Existing" "Instance" global hint_info +| "Existing" "Instances" global_list natural_opt2 +| "Existing" "Class" global +| "Arguments" smart_global argument_spec_block_list_opt more_implicits_block_opt arguments_modifier_opt +| "Implicit" "Type" reserv_list +| "Implicit" "Types" reserv_list +| "Generalizable" All_alt +| "Export" "Set" option_table option_setting +| "Export" "Unset" option_table +| "Import" "Prenex" "Implicits" (* ssr plugin *) +] + +module_binder_list_opt: [ +| module_binder_list_opt module_binder +| empty +] + +ext_module_expr_list_opt: [ +| ext_module_expr_list_opt ext_module_expr +| empty +] + +ext_module_type_list_opt: [ +| ext_module_type_list_opt ext_module_type +| empty +] + +strategy_level_list: [ +| strategy_level_list strategy_level "[" smart_global_list "]" +| strategy_level "[" smart_global_list "]" +] + +Structure_opt: [ +| "Structure" +| empty +] + +univ_decl_opt: [ +| univ_decl +| empty +] + +binder_list: [ +| binder_list binder +| binder +] + +record_declaration_opt: [ +| ":=" "{" record_declaration "}" +| ":=" lconstr +| empty +] + +natural_opt: [ +| natural +| empty +] + +argument_spec_block_list_opt: [ +| argument_spec_block_list_opt argument_spec_block +| empty +] + +more_implicits_block_opt: [ +| "," more_implicits_block_list_comma +| empty +] + +more_implicits_block_list_comma: [ +| more_implicits_block_list_comma "," more_implicits_block_list_opt +| more_implicits_block_list_opt +] + +arguments_modifier_opt: [ +| ":" arguments_modifier_list_comma +| empty +] + +arguments_modifier_list_comma: [ +| arguments_modifier_list_comma "," arguments_modifier +| arguments_modifier +] + +All_alt: [ +| "All" "Variables" +| "No" "Variables" +| Variable_alt ident_list +] + +Variable_alt: [ +| "Variable" +| "Variables" +] + +more_implicits_block_list_opt: [ +| more_implicits_block_list_opt more_implicits_block +| empty +] + +univ_decl_opt2: [ +| univ_decl_opt def_body +| empty +] + +export_token: [ +| "Import" +| "Export" +| empty +] + +ext_module_type: [ +| "<+" module_type_inl +] + +ext_module_expr: [ +| "<+" module_expr_inl +] + +check_module_type: [ +| "<:" module_type_inl +] + +check_module_types: [ +| check_module_type_list_opt +] + +check_module_type_list_opt: [ +| check_module_type_list_opt check_module_type +| empty +] + +of_module_type: [ +| ":" module_type_inl +| check_module_types +] + +is_module_type: [ +| ":=" module_type_inl ext_module_type_list_opt +| empty +] + +is_module_expr: [ +| ":=" module_expr_inl ext_module_expr_list_opt +| empty +] + +functor_app_annot: [ +| "[" "inline" "at" "level" natural "]" +| "[" "no" "inline" "]" +| empty +] + +module_expr_inl: [ +| "!" module_expr +| module_expr functor_app_annot +] + +module_type_inl: [ +| "!" module_type +| module_type functor_app_annot +] + +module_binder: [ +| "(" export_token ident_list ":" module_type_inl ")" +] + +module_expr: [ +| module_expr_atom +| module_expr module_expr_atom +] + +module_expr_atom: [ +| qualid +| "(" module_expr ")" +] + +with_declaration: [ +| "Definition" fullyqualid univ_decl_opt ":=" lconstr +| "Module" fullyqualid ":=" qualid +] + +module_type: [ +| qualid +| "(" module_type ")" +| module_type module_expr_atom +| module_type "with" with_declaration +] + +section_subset_expr: [ +| starredidentref_list_opt +| ssexpr35 +] + +starredidentref_list_opt: [ +| starredidentref_list_opt starredidentref +| empty +] + +starredidentref: [ +| ident +| ident "*" +| "Type" +| "Type" "*" +] + +ssexpr35: [ +| "-" ssexpr50 +| ssexpr50 +] + +ssexpr50: [ +| ssexpr0 "-" ssexpr0 +| ssexpr0 "+" ssexpr0 +| ssexpr0 +] + +ssexpr0: [ +| starredidentref +| "(" starredidentref_list_opt ")" +| "(" starredidentref_list_opt ")" "*" +| "(" ssexpr35 ")" +| "(" ssexpr35 ")" "*" +] + +arguments_modifier: [ +| "simpl" "nomatch" +| "simpl" "never" +| "default" "implicits" +| "clear" "implicits" +| "clear" "scopes" +| "clear" "bidirectionality" "hint" +| "rename" +| "assert" +| "extra" "scopes" +| "clear" "scopes" "and" "implicits" +| "clear" "implicits" "and" "scopes" +] + +scope: [ +| "%" IDENT +] + +argument_spec: [ +| exclam_opt name scope_opt +] + +exclam_opt: [ +| "!" +| empty +] + +scope_opt: [ +| scope +| empty +] + +argument_spec_block: [ +| argument_spec +| "/" +| "&" +| "(" argument_spec_list ")" scope_opt +| "[" argument_spec_list "]" scope_opt +| "{" argument_spec_list "}" scope_opt +] + +argument_spec_list: [ +| argument_spec_list argument_spec +| argument_spec +] + +more_implicits_block: [ +| name +| "[" name_list "]" +| "{" name_list "}" +] + +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +] + +instance_name: [ +| ident_decl binders +| empty +] + +hint_info: [ +| "|" natural_opt constr_pattern_opt +| empty +] + +reserv_list: [ +| reserv_tuple_list +| simple_reserv +] + +reserv_tuple_list: [ +| reserv_tuple_list reserv_tuple +| reserv_tuple +] + +reserv_tuple: [ +| "(" simple_reserv ")" +] + +simple_reserv: [ +| ident_list ":" lconstr +] + +command: [ +| "Comments" comment_list_opt +| "Declare" "Instance" ident_decl binders ":" operconstr200 hint_info +| "Declare" "Scope" IDENT +| "Pwd" +| "Cd" +| "Cd" ne_string +| "Load" Verbose_opt ne_string_alt +| "Declare" "ML" "Module" ne_string_list +| "Locate" locatable +| "Add" "LoadPath" ne_string as_dirpath +| "Add" "Rec" "LoadPath" ne_string as_dirpath +| "Remove" "LoadPath" ne_string +| "AddPath" ne_string "as" as_dirpath +| "AddRecPath" ne_string "as" as_dirpath +| "DelPath" ne_string +| "Type" lconstr +| "Print" printable +| "Print" smart_global univ_name_list_opt +| "Print" "Module" "Type" global +| "Print" "Module" global +| "Print" "Namespace" dirpath +| "Inspect" natural +| "Add" "ML" "Path" ne_string +| "Add" "Rec" "ML" "Path" ne_string +| "Set" option_table option_setting +| "Unset" option_table +| "Print" "Table" option_table +| "Add" IDENT IDENT option_ref_value_list +| "Add" IDENT option_ref_value_list +| "Test" option_table "for" option_ref_value_list +| "Test" option_table +| "Remove" IDENT IDENT option_ref_value_list +| "Remove" IDENT option_ref_value_list +| "Write" "State" IDENT +| "Write" "State" ne_string +| "Restore" "State" IDENT +| "Restore" "State" ne_string +| "Reset" "Initial" +| "Reset" ident +| "Back" +| "Back" natural +| "BackTo" natural +| "Debug" "On" +| "Debug" "Off" +| "Declare" "Reduction" IDENT; ":=" red_expr +| "Declare" "Custom" "Entry" IDENT +| "Goal" lconstr +| "Proof" +| "Proof" "Mode" string +| "Proof" lconstr +| "Abort" +| "Abort" "All" +| "Abort" ident +| "Existential" natural constr_body +| "Admitted" +| "Qed" +| "Save" ident +| "Defined" +| "Defined" ident +| "Restart" +| "Undo" +| "Undo" natural +| "Undo" "To" natural +| "Focus" +| "Focus" natural +| "Unfocus" +| "Unfocused" +| "Show" +| "Show" natural +| "Show" ident +| "Show" "Existentials" +| "Show" "Universes" +| "Show" "Conjectures" +| "Show" "Proof" +| "Show" "Intro" +| "Show" "Intros" +| "Show" "Match" reference +| "Guarded" +| "Create" "HintDb" IDENT discriminated_opt +| "Remove" "Hints" global_list opt_hintbases +| "Hint" hint opt_hintbases +| "Obligation" integer "of" ident ":" lglob withtac +| "Obligation" integer "of" ident withtac +| "Obligation" integer ":" lglob withtac +| "Obligation" integer withtac +| "Next" "Obligation" "of" ident withtac +| "Next" "Obligation" withtac +| "Solve" "Obligation" integer "of" ident "with" tactic +| "Solve" "Obligation" integer "with" tactic +| "Solve" "Obligations" "of" ident "with" tactic +| "Solve" "Obligations" "with" tactic +| "Solve" "Obligations" +| "Solve" "All" "Obligations" "with" tactic +| "Solve" "All" "Obligations" +| "Admit" "Obligations" "of" ident +| "Admit" "Obligations" +| "Obligation" "Tactic" ":=" tactic +| "Show" "Obligation" "Tactic" +| "Obligations" "of" ident +| "Obligations" +| "Preterm" "of" ident +| "Preterm" +| "Hint" "Rewrite" orient term_list ":" preident_list_opt +| "Hint" "Rewrite" orient term_list "using" tactic ":" preident_list_opt +| "Hint" "Rewrite" orient term_list +| "Hint" "Rewrite" orient term_list "using" tactic +| "Derive" "Inversion_clear" ident "with" term "Sort" sort_family +| "Derive" "Inversion_clear" ident "with" term +| "Derive" "Inversion" ident "with" term "Sort" sort_family +| "Derive" "Inversion" ident "with" term +| "Derive" "Dependent" "Inversion" ident "with" term "Sort" sort_family +| "Derive" "Dependent" "Inversion_clear" ident "with" term "Sort" sort_family +| "Declare" "Left" "Step" term +| "Declare" "Right" "Step" term +| "Grab" "Existential" "Variables" +| "Unshelve" +| "Declare" "Equivalent" "Keys" term term +| "Print" "Equivalent" "Keys" +| "Optimize" "Proof" +| "Optimize" "Heap" +| "Reset" "Ltac" "Profile" +| "Show" "Ltac" "Profile" +| "Show" "Ltac" "Profile" "CutOff" int +| "Show" "Ltac" "Profile" string +| "Hint" "Cut" "[" hints_path "]" opthints +| "Typeclasses" "Transparent" reference_list_opt +| "Typeclasses" "Opaque" reference_list_opt +| "Typeclasses" "eauto" ":=" debug eauto_search_strategy int_opt +| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "as" ident +| "Add" "Relation" term term "symmetry" "proved" "by" term "as" ident +| "Add" "Relation" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Relation" term term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "reflexivity" "proved" "by" term "symmetry" "proved" "by" term "transitivity" "proved" "by" term "as" ident +| "Add" "Parametric" "Relation" binders ":" term term "transitivity" "proved" "by" term "as" ident +| "Add" "Setoid" term term term "as" ident +| "Add" "Parametric" "Setoid" binders ":" term term term "as" ident +| "Add" "Morphism" term ":" ident +| "Declare" "Morphism" term ":" ident +| "Add" "Morphism" term "with" "signature" lconstr "as" ident +| "Add" "Parametric" "Morphism" binders ":" term "with" "signature" lconstr "as" ident +| "Print" "Rewrite" "HintDb" preident +| "Proof" "with" tactic using_opt +| "Proof" "using" section_subset_expr with_opt +| "Tactic" "Notation" ltac_tactic_level_opt ltac_production_item_list ":=" tactic +| "Print" "Ltac" reference +| "Locate" "Ltac" reference +| "Ltac" ltac_tacdef_body_list +| "Print" "Ltac" "Signatures" +| "String" "Notation" reference reference reference ":" ident +| "Set" "Firstorder" "Solver" tactic +| "Print" "Firstorder" "Solver" +| "Numeral" "Notation" reference reference reference ":" ident numnotoption +| "Derive" ident "SuchThat" term "As" ident (* derive plugin *) +| "Extraction" global (* extraction plugin *) +| "Recursive" "Extraction" global_list (* extraction plugin *) +| "Extraction" string global_list (* extraction plugin *) +| "Extraction" "TestCompile" global_list (* extraction plugin *) +| "Separate" "Extraction" global_list (* extraction plugin *) +| "Extraction" "Library" ident (* extraction plugin *) +| "Recursive" "Extraction" "Library" ident (* extraction plugin *) +| "Extraction" "Language" language (* extraction plugin *) +| "Extraction" "Inline" global_list (* extraction plugin *) +| "Extraction" "NoInline" global_list (* extraction plugin *) +| "Print" "Extraction" "Inline" (* extraction plugin *) +| "Reset" "Extraction" "Inline" (* extraction plugin *) +| "Extraction" "Implicit" global "[" int_or_id_list_opt "]" (* extraction plugin *) +| "Extraction" "Blacklist" ident_list (* extraction plugin *) +| "Print" "Extraction" "Blacklist" (* extraction plugin *) +| "Reset" "Extraction" "Blacklist" (* extraction plugin *) +| "Extract" "Constant" global string_list_opt "=>" mlname (* extraction plugin *) +| "Extract" "Inlined" "Constant" global "=>" mlname (* extraction plugin *) +| "Extract" "Inductive" global "=>" mlname "[" mlname_list_opt "]" string_opt (* extraction plugin *) +| "Show" "Extraction" (* extraction plugin *) +| "Function" function_rec_definition_loc_list (* funind plugin *) +| "Functional" "Scheme" fun_scheme_arg_list (* funind plugin *) +| "Functional" "Case" fun_scheme_arg (* funind plugin *) +| "Generate" "graph" "for" reference (* funind plugin *) +| "Add" "Ring" ident ":" term ring_mods_opt (* setoid_ring plugin *) +| "Print" "Rings" (* setoid_ring plugin *) +| "Add" "Field" ident ":" term field_mods_opt (* setoid_ring plugin *) +| "Print" "Fields" (* setoid_ring plugin *) +| "Prenex" "Implicits" global_list (* ssr plugin *) +| "Search" ssr_search_arg ssr_modlocs (* ssr plugin *) +| "Print" "Hint" "View" ssrviewpos (* ssr plugin *) +| "Hint" "View" ssrviewposspc ssrhintref_list (* ssr plugin *) +] + +comment_list_opt: [ +| comment_list_opt comment +| empty +] + +Verbose_opt: [ +| "Verbose" +| empty +] + +ne_string_alt: [ +| ne_string +| IDENT +] + +ne_string_list: [ +| ne_string_list ne_string +| ne_string +] + +univ_name_list_opt: [ +| univ_name_list +| empty +] + +option_ref_value_list: [ +| option_ref_value_list option_ref_value +| option_ref_value +] + +discriminated_opt: [ +| "discriminated" +| empty +] + +global_list: [ +| global_list global +| global +] + +preident_list_opt: [ +| preident_list_opt preident +| empty +] + +reference_list_opt: [ +| reference_list_opt reference +| empty +] + +int_opt: [ +| int +| empty +] + +using_opt: [ +| "using" section_subset_expr +| empty +] + +with_opt: [ +| "with" tactic +| empty +] + +ltac_tactic_level_opt: [ +| ltac_tactic_level +| empty +] + +ltac_production_item_list: [ +| ltac_production_item_list ltac_production_item +| ltac_production_item +] + +ltac_tacdef_body_list: [ +| ltac_tacdef_body_list "with" ltac_tacdef_body +| ltac_tacdef_body +] + +int_or_id_list_opt: [ +| int_or_id_list_opt int_or_id +| empty +] + +ident_list: [ +| ident_list ident +| ident +] + +string_list_opt: [ +| string_list_opt string +| empty +] + +mlname_list_opt: [ +| mlname_list_opt mlname +| empty +] + +string_opt: [ +| string +| empty +] + +function_rec_definition_loc_list: [ +| function_rec_definition_loc_list "with" function_rec_definition_loc +| function_rec_definition_loc +] + +fun_scheme_arg_list: [ +| fun_scheme_arg_list "with" fun_scheme_arg +| fun_scheme_arg +] + +ring_mods_opt: [ +| ring_mods +| empty +] + +field_mods_opt: [ +| field_mods +| empty +] + +ssrhintref_list: [ +| ssrhintref_list ssrhintref +| ssrhintref +] + +query_command: [ +| "Eval" red_expr "in" lconstr "." +| "Compute" lconstr "." +| "Check" lconstr "." +| "About" smart_global univ_name_list_opt "." +| "SearchHead" constr_pattern in_or_out_modules "." +| "SearchPattern" constr_pattern in_or_out_modules "." +| "SearchRewrite" constr_pattern in_or_out_modules "." +| "Search" searchabout_query searchabout_queries "." +| "SearchAbout" searchabout_query searchabout_queries "." +| "SearchAbout" "[" searchabout_query_list "]" in_or_out_modules "." +] + +searchabout_query_list: [ +| searchabout_query_list searchabout_query +| searchabout_query +] + +printable: [ +| "Term" smart_global univ_name_list_opt +| "All" +| "Section" global +| "Grammar" IDENT +| "Custom" "Grammar" IDENT +| "LoadPath" dirpath_opt +| "Modules" +| "Libraries" +| "ML" "Path" +| "ML" "Modules" +| "Debug" "GC" +| "Graph" +| "Classes" +| "TypeClasses" +| "Instances" smart_global +| "Coercions" +| "Coercion" "Paths" class_rawexpr class_rawexpr +| "Canonical" "Projections" +| "Tables" +| "Options" +| "Hint" +| "Hint" smart_global +| "Hint" "*" +| "HintDb" IDENT +| "Scopes" +| "Scope" IDENT +| "Visibility" IDENT_opt3 +| "Implicit" smart_global +| Sorted_opt "Universes" printunivs_subgraph_opt ne_string_opt +| "Assumptions" smart_global +| "Opaque" "Dependencies" smart_global +| "Transparent" "Dependencies" smart_global +| "All" "Dependencies" smart_global +| "Strategy" smart_global +| "Strategies" +| "Registered" +] + +dirpath_opt: [ +| dirpath +| empty +] + +IDENT_opt3: [ +| IDENT +| empty +] + +Sorted_opt: [ +| "Sorted" +| empty +] + +printunivs_subgraph_opt: [ +| printunivs_subgraph +| empty +] + +ne_string_opt: [ +| ne_string +| empty +] + +printunivs_subgraph: [ +| "Subgraph" "(" reference_list_opt ")" +] + +class_rawexpr: [ +| "Funclass" +| "Sortclass" +| smart_global +] + +locatable: [ +| smart_global +| "Term" smart_global +| "File" ne_string +| "Library" global +| "Module" global +] + +option_setting: [ +| empty +| integer +| STRING +] + +option_ref_value: [ +| global +| STRING +] + +option_table: [ +| IDENT_list +] + +as_dirpath: [ +| as_opt3 +] + +as_opt: [ +| "as" name +| empty +] + +ne_in_or_out_modules: [ +| "inside" global_list +| "outside" global_list +] + +in_or_out_modules: [ +| ne_in_or_out_modules +| empty +] + +comment: [ +| term +| STRING +| natural +] + +positive_search_mark: [ +| "-" +| empty +] + +searchabout_query: [ +| positive_search_mark ne_string scope_opt +| positive_search_mark constr_pattern +] + +searchabout_queries: [ +| ne_in_or_out_modules +| searchabout_query searchabout_queries +| empty +] + +univ_name_list: [ +| "@{" name_list_opt "}" +] + +syntax: [ +| "Open" "Scope" IDENT +| "Close" "Scope" IDENT +| "Delimit" "Scope" IDENT; "with" IDENT +| "Undelimit" "Scope" IDENT +| "Bind" "Scope" IDENT; "with" class_rawexpr_list +| "Infix" ne_lstring ":=" term syntax_modifier_opt IDENT_opt2 +| "Notation" ident ident_list_opt ":=" term only_parsing +| "Notation" lstring ":=" term syntax_modifier_opt IDENT_opt2 +| "Format" "Notation" STRING STRING STRING +| "Reserved" "Infix" ne_lstring syntax_modifier_opt +| "Reserved" "Notation" ne_lstring syntax_modifier_opt +] + +class_rawexpr_list: [ +| class_rawexpr_list class_rawexpr +| class_rawexpr +] + +syntax_modifier_opt: [ +| "(" syntax_modifier_list_comma ")" +| empty +] + +syntax_modifier_list_comma: [ +| syntax_modifier_list_comma "," syntax_modifier +| syntax_modifier +] + +only_parsing: [ +| "(" "only" "parsing" ")" +| "(" "compat" STRING ")" +| empty +] + +level: [ +| "level" natural +| "next" "level" +] + +syntax_modifier: [ +| "at" "level" natural +| "in" "custom" IDENT +| "in" "custom" IDENT; "at" "level" natural +| "left" "associativity" +| "right" "associativity" +| "no" "associativity" +| "only" "printing" +| "only" "parsing" +| "compat" STRING +| "format" STRING STRING_opt +| IDENT; "," IDENT_list_comma "at" level +| IDENT; "at" level +| IDENT; "at" level constr_as_binder_kind +| IDENT constr_as_binder_kind +| IDENT syntax_extension_type +] + +STRING_opt: [ +| STRING +| empty +] + +IDENT_list_comma: [ +| IDENT_list_comma "," IDENT +| IDENT +] + +syntax_extension_type: [ +| "ident" +| "global" +| "bigint" +| "binder" +| "constr" +| "constr" at_level_opt constr_as_binder_kind_opt +| "pattern" +| "pattern" "at" "level" natural +| "strict" "pattern" +| "strict" "pattern" "at" "level" natural +| "closed" "binder" +| "custom" IDENT at_level_opt constr_as_binder_kind_opt +] + +at_level_opt: [ +| at_level +| empty +] + +constr_as_binder_kind_opt: [ +| constr_as_binder_kind +| empty +] + +at_level: [ +| "at" level +] + +constr_as_binder_kind: [ +| "as" "ident" +| "as" "pattern" +| "as" "strict" "pattern" +] + +opt_hintbases: [ +| empty +| ":" IDENT_list +] + +IDENT_list: [ +| IDENT_list IDENT +| IDENT +] + +reference_or_constr: [ +| global +| term +] + +hint: [ +| "Resolve" reference_or_constr_list hint_info +| "Resolve" "->" global_list natural_opt +| "Resolve" "<-" global_list natural_opt +| "Immediate" reference_or_constr_list +| "Variables" "Transparent" +| "Variables" "Opaque" +| "Constants" "Transparent" +| "Constants" "Opaque" +| "Transparent" global_list +| "Opaque" global_list +| "Mode" global mode +| "Unfold" global_list +| "Constructors" global_list +| "Extern" natural constr_pattern_opt "=>" tactic +] + +reference_or_constr_list: [ +| reference_or_constr_list reference_or_constr +| reference_or_constr +] + +natural_opt2: [ +| "|" natural +| empty +] + +constr_pattern_opt: [ +| constr_pattern +| empty +] + +constr_body: [ +| ":=" lconstr +| ":" lconstr ":=" lconstr +] + +mode: [ +| plus_list +] + +plus_list: [ +| plus_list plus_alt +| plus_alt +] + +plus_alt: [ +| "+" +| "!" +| "-" +] + +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "Backtrack" natural natural natural "." +| "Show" "Goal" natural "at" natural "." +| vernac_control +] + +orient: [ +| "->" +| "<-" +| empty +] + +occurrences: [ +| integer_list +| var +] + +integer_list: [ +| integer_list integer +| integer +] + +glob: [ +| term +] + +lglob: [ +| lconstr +] + +casted_constr: [ +| term +] + +hloc: [ +| empty +| "in" "|-" "*" +| "in" ident +| "in" "(" "Type" "of" ident ")" +| "in" "(" "Value" "of" ident ")" +| "in" "(" "type" "of" ident ")" +| "in" "(" "value" "of" ident ")" +] + +rename: [ +| ident "into" ident +] + +by_arg_tac: [ +| "by" ltac_expr3 +| empty +] + +in_clause: [ +| in_clause +| "*" occs +| "*" "|-" concl_occ +| hypident_occ_list_comma_opt "|-" concl_occ +| hypident_occ_list_comma_opt +] + +hypident_occ_list_comma_opt: [ +| hypident_occ_list_comma +| empty +] + +hypident_occ_list_comma: [ +| hypident_occ_list_comma "," hypident_occ +| hypident_occ +] + +test_lpar_id_colon: [ +| empty +] + +withtac: [ +| "with" tactic +| empty +] + +closed_binder: [ +| "(" name name_list ":" lconstr ")" +| "(" name ":" lconstr ")" +| "(" name ":=" lconstr ")" +| "(" name ":" lconstr ":=" lconstr ")" +| "{" name "}" +| "{" name name_list ":" lconstr "}" +| "{" name ":" lconstr "}" +| "{" name name_list "}" +| "`(" typeclass_constraint_list_comma ")" +| "`{" typeclass_constraint_list_comma "}" +| "'" pattern0 +| of_alt operconstr99 (* ssr plugin *) +| "(" "_" ":" lconstr "|" lconstr ")" +] + +typeclass_constraint_list_comma: [ +| typeclass_constraint_list_comma "," typeclass_constraint +| typeclass_constraint +] + +of_alt: [ +| "of" +| "&" +] + +simple_tactic: [ +| "reflexivity" +| "exact" casted_constr +| "assumption" +| "etransitivity" +| "cut" term +| "exact_no_check" term +| "vm_cast_no_check" term +| "native_cast_no_check" term +| "casetype" term +| "elimtype" term +| "lapply" term +| "transitivity" term +| "left" +| "eleft" +| "left" "with" bindings +| "eleft" "with" bindings +| "right" +| "eright" +| "right" "with" bindings +| "eright" "with" bindings +| "constructor" +| "constructor" int_or_var +| "constructor" int_or_var "with" bindings +| "econstructor" +| "econstructor" int_or_var +| "econstructor" int_or_var "with" bindings +| "specialize" constr_with_bindings +| "specialize" constr_with_bindings "as" simple_intropattern +| "symmetry" +| "symmetry" "in" in_clause +| "split" +| "esplit" +| "split" "with" bindings +| "esplit" "with" bindings +| "exists" +| "exists" bindings_list_comma +| "eexists" +| "eexists" bindings_list_comma +| "intros" "until" quantified_hypothesis +| "intro" +| "intro" ident +| "intro" ident "at" "top" +| "intro" ident "at" "bottom" +| "intro" ident "after" var +| "intro" ident "before" var +| "intro" "at" "top" +| "intro" "at" "bottom" +| "intro" "after" var +| "intro" "before" var +| "move" var "at" "top" +| "move" var "at" "bottom" +| "move" var "after" var +| "move" var "before" var +| "rename" rename_list_comma +| "revert" var_list +| "simple" "induction" quantified_hypothesis +| "simple" "destruct" quantified_hypothesis +| "double" "induction" quantified_hypothesis quantified_hypothesis +| "admit" +| "fix" ident natural +| "cofix" ident +| "clear" var_list_opt +| "clear" "-" var_list +| "clearbody" var_list +| "generalize" "dependent" term +| "replace" uconstr "with" term clause_dft_concl by_arg_tac +| "replace" "->" uconstr clause_dft_concl +| "replace" "<-" uconstr clause_dft_concl +| "replace" uconstr clause_dft_concl +| "simplify_eq" +| "simplify_eq" destruction_arg +| "esimplify_eq" +| "esimplify_eq" destruction_arg +| "discriminate" +| "discriminate" destruction_arg +| "ediscriminate" +| "ediscriminate" destruction_arg +| "injection" +| "injection" destruction_arg +| "einjection" +| "einjection" destruction_arg +| "injection" "as" simple_intropattern_list_opt +| "injection" destruction_arg "as" simple_intropattern_list_opt +| "einjection" "as" simple_intropattern_list_opt +| "einjection" destruction_arg "as" simple_intropattern_list_opt +| "simple" "injection" +| "simple" "injection" destruction_arg +| "dependent" "rewrite" orient term +| "dependent" "rewrite" orient term "in" var +| "cutrewrite" orient term +| "cutrewrite" orient term "in" var +| "decompose" "sum" term +| "decompose" "record" term +| "absurd" term +| "contradiction" constr_with_bindings_opt +| "autorewrite" "with" preident_list clause_dft_concl +| "autorewrite" "with" preident_list clause_dft_concl "using" tactic +| "autorewrite" "*" "with" preident_list clause_dft_concl +| "autorewrite" "*" "with" preident_list clause_dft_concl "using" tactic +| "rewrite" "*" orient uconstr "in" var "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences "in" var by_arg_tac +| "rewrite" "*" orient uconstr "in" var by_arg_tac +| "rewrite" "*" orient uconstr "at" occurrences by_arg_tac +| "rewrite" "*" orient uconstr by_arg_tac +| "refine" uconstr +| "simple" "refine" uconstr +| "notypeclasses" "refine" uconstr +| "simple" "notypeclasses" "refine" uconstr +| "solve_constraints" +| "subst" var_list +| "subst" +| "simple" "subst" +| "evar" test_lpar_id_colon "(" ident ":" lconstr ")" +| "evar" term +| "instantiate" "(" ident ":=" lglob ")" +| "instantiate" "(" integer ":=" lglob ")" hloc +| "instantiate" +| "stepl" term "by" tactic +| "stepl" term +| "stepr" term "by" tactic +| "stepr" term +| "generalize_eqs" var +| "dependent" "generalize_eqs" var +| "generalize_eqs_vars" var +| "dependent" "generalize_eqs_vars" var +| "specialize_eqs" var +| "hresolve_core" "(" ident ":=" term ")" "at" int_or_var "in" term +| "hresolve_core" "(" ident ":=" term ")" "in" term +| "hget_evar" int_or_var +| "destauto" +| "destauto" "in" var +| "transparent_abstract" ltac_expr3 +| "transparent_abstract" ltac_expr3 "using" ident +| "constr_eq" term term +| "constr_eq_strict" term term +| "constr_eq_nounivs" term term +| "is_evar" term +| "has_evar" term +| "is_var" term +| "is_fix" term +| "is_cofix" term +| "is_ind" term +| "is_constructor" term +| "is_proj" term +| "is_const" term +| "shelve" +| "shelve_unifiable" +| "unshelve" ltac_expr1 +| "give_up" +| "cycle" int_or_var +| "swap" int_or_var int_or_var +| "revgoals" +| "guard" test +| "decompose" "[" term_list "]" term +| "optimize_heap" +| "start" "ltac" "profiling" +| "stop" "ltac" "profiling" +| "reset" "ltac" "profile" +| "show" "ltac" "profile" +| "show" "ltac" "profile" "cutoff" int +| "show" "ltac" "profile" string +| "restart_timer" string_opt +| "finish_timing" string_opt +| "finish_timing" "(" string ")" string_opt +| "eassumption" +| "eexact" term +| "trivial" auto_using hintbases +| "info_trivial" auto_using hintbases +| "debug" "trivial" auto_using hintbases +| "auto" int_or_var_opt auto_using hintbases +| "info_auto" int_or_var_opt auto_using hintbases +| "debug" "auto" int_or_var_opt auto_using hintbases +| "prolog" "[" uconstr_list_opt "]" int_or_var +| "eauto" int_or_var_opt int_or_var_opt auto_using hintbases +| "new" "auto" int_or_var_opt auto_using hintbases +| "debug" "eauto" int_or_var_opt int_or_var_opt auto_using hintbases +| "info_eauto" int_or_var_opt int_or_var_opt auto_using hintbases +| "dfs" "eauto" int_or_var_opt auto_using hintbases +| "autounfold" hintbases clause_dft_concl +| "autounfold_one" hintbases "in" var +| "autounfold_one" hintbases +| "unify" term term +| "unify" term term "with" preident +| "convert_concl_no_check" term +| "typeclasses" "eauto" "bfs" int_or_var_opt "with" preident_list +| "typeclasses" "eauto" int_or_var_opt "with" preident_list +| "typeclasses" "eauto" int_or_var_opt +| "head_of_constr" ident term +| "not_evar" term +| "is_ground" term +| "autoapply" term "using" preident +| "autoapply" term "with" preident +| "progress_evars" tactic +| "rewrite_strat" rewstrategy "in" var +| "rewrite_strat" rewstrategy +| "rewrite_db" preident "in" var +| "rewrite_db" preident +| "substitute" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings +| "setoid_rewrite" orient glob_constr_with_bindings "in" var +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences +| "setoid_rewrite" orient glob_constr_with_bindings "at" occurrences "in" var +| "setoid_rewrite" orient glob_constr_with_bindings "in" var "at" occurrences +| "setoid_symmetry" +| "setoid_symmetry" "in" var +| "setoid_reflexivity" +| "setoid_transitivity" term +| "setoid_etransitivity" +| "decide" "equality" +| "compare" term term +| "intros" intropattern_list_opt +| "eintros" intropattern_list_opt +| "apply" constr_with_bindings_arg_list_comma in_hyp_as +| "eapply" constr_with_bindings_arg_list_comma in_hyp_as +| "simple" "apply" constr_with_bindings_arg_list_comma in_hyp_as +| "simple" "eapply" constr_with_bindings_arg_list_comma in_hyp_as +| "elim" constr_with_bindings_arg eliminator_opt +| "eelim" constr_with_bindings_arg eliminator_opt +| "case" induction_clause_list +| "ecase" induction_clause_list +| "fix" ident natural "with" fixdecl_list +| "cofix" ident "with" cofixdecl_list +| "pose" bindings_with_parameters +| "pose" term as_name +| "epose" bindings_with_parameters +| "epose" term as_name +| "set" bindings_with_parameters clause_dft_concl +| "set" term as_name clause_dft_concl +| "eset" bindings_with_parameters clause_dft_concl +| "eset" term as_name clause_dft_concl +| "remember" term as_name eqn_ipat clause_dft_all +| "eremember" term as_name eqn_ipat clause_dft_all +| "assert" "(" ident ":=" lconstr ")" +| "eassert" "(" ident ":=" lconstr ")" +| "assert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "eassert" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "enough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "eenough" test_lpar_id_colon "(" ident ":" lconstr ")" by_tactic +| "assert" term as_ipat by_tactic +| "eassert" term as_ipat by_tactic +| "pose" "proof" lconstr as_ipat +| "epose" "proof" lconstr as_ipat +| "enough" term as_ipat by_tactic +| "eenough" term as_ipat by_tactic +| "generalize" term +| "generalize" term term_list +| "generalize" term occs as_name pattern_occ_list_opt +| "induction" induction_clause_list +| "einduction" induction_clause_list +| "destruct" induction_clause_list +| "edestruct" induction_clause_list +| "rewrite" oriented_rewriter_list_comma clause_dft_concl by_tactic +| "erewrite" oriented_rewriter_list_comma clause_dft_concl by_tactic +| "dependent" simple_alt quantified_hypothesis as_or_and_ipat with_opt2 +| "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list +| "inversion" quantified_hypothesis "using" term in_hyp_list +| "red" clause_dft_concl +| "hnf" clause_dft_concl +| "simpl" delta_flag ref_or_pattern_occ_opt clause_dft_concl +| "cbv" strategy_flag clause_dft_concl +| "cbn" strategy_flag clause_dft_concl +| "lazy" strategy_flag clause_dft_concl +| "compute" delta_flag clause_dft_concl +| "vm_compute" ref_or_pattern_occ_opt clause_dft_concl +| "native_compute" ref_or_pattern_occ_opt clause_dft_concl +| "unfold" unfold_occ_list_comma clause_dft_concl +| "fold" term_list clause_dft_concl +| "pattern" pattern_occ_list_comma clause_dft_concl +| "change" conversion clause_dft_concl +| "change_no_check" conversion clause_dft_concl +| "btauto" +| "rtauto" +| "congruence" +| "congruence" integer +| "congruence" "with" term_list +| "congruence" integer "with" term_list +| "f_equal" +| "firstorder" tactic_opt firstorder_using +| "firstorder" tactic_opt "with" preident_list +| "firstorder" tactic_opt firstorder_using "with" preident_list +| "gintuition" tactic_opt +| "functional" "inversion" quantified_hypothesis reference_opt (* funind plugin *) +| "functional" "induction" term_list fun_ind_using with_names (* funind plugin *) +| "soft" "functional" "induction" term_list fun_ind_using with_names (* funind plugin *) +| "myred" (* micromega plugin *) +| "psatz_Z" int_or_var tactic (* micromega plugin *) +| "psatz_Z" tactic (* micromega plugin *) +| "xlia" tactic (* micromega plugin *) +| "xnlia" tactic (* micromega plugin *) +| "xnra" tactic (* micromega plugin *) +| "xnqa" tactic (* micromega plugin *) +| "sos_Z" tactic (* micromega plugin *) +| "sos_Q" tactic (* micromega plugin *) +| "sos_R" tactic (* micromega plugin *) +| "lra_Q" tactic (* micromega plugin *) +| "lra_R" tactic (* micromega plugin *) +| "psatz_R" int_or_var tactic (* micromega plugin *) +| "psatz_R" tactic (* micromega plugin *) +| "psatz_Q" int_or_var tactic (* micromega plugin *) +| "psatz_Q" tactic (* micromega plugin *) +| "nsatz_compute" term (* nsatz plugin *) +| "omega" (* omega plugin *) +| "omega" "with" ident_list (* omega plugin *) +| "omega" "with" "*" (* omega plugin *) +| "protect_fv" string "in" ident (* setoid_ring plugin *) +| "protect_fv" string (* setoid_ring plugin *) +| "ring_lookup" ltac_expr0 "[" term_list_opt "]" term_list (* setoid_ring plugin *) +| "field_lookup" tactic "[" term_list_opt "]" term_list (* setoid_ring plugin *) +| "YouShouldNotTypeThis" ssrintrosarg (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +| "YouShouldNotTypeThis" "do" (* ssr plugin *) +| "YouShouldNotTypeThis" ssrtclarg ssrseqarg (* ssr plugin *) +| "clear" natural (* ssr plugin *) +| "move" ssrmovearg ssrrpat (* ssr plugin *) +| "move" ssrmovearg ssrclauses (* ssr plugin *) +| "move" ssrrpat (* ssr plugin *) +| "move" (* ssr plugin *) +| "case" ssrcasearg ssrclauses (* ssr plugin *) +| "case" (* ssr plugin *) +| "elim" ssrarg ssrclauses (* ssr plugin *) +| "elim" (* ssr plugin *) +| "apply" ssrapplyarg (* ssr plugin *) +| "apply" (* ssr plugin *) +| "exact" ssrexactarg (* ssr plugin *) +| "exact" (* ssr plugin *) +| "exact" "<:" lconstr (* ssr plugin *) +| "congr" ssrcongrarg (* ssr plugin *) +| "ssrinstancesofruleL2R" ssrterm (* ssr plugin *) +| "ssrinstancesofruleR2L" ssrterm (* ssr plugin *) +| "rewrite" ssrrwargs ssrclauses (* ssr plugin *) +| "unlock" ssrunlockargs ssrclauses (* ssr plugin *) +| "pose" ssrfixfwd (* ssr plugin *) +| "pose" ssrcofixfwd (* ssr plugin *) +| "pose" ssrfwdid ssrposefwd (* ssr plugin *) +| "set" ssrfwdid ssrsetfwd ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| "have" ssrhavefwdwbinders (* ssr plugin *) +| "have" "suff" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "have" "suffices" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suffices" "have" ssrhpats_nobs ssrhavefwd (* ssr plugin *) +| "suff" ssrsufffwd (* ssr plugin *) +| "suffices" ssrsufffwd (* ssr plugin *) +| "wlog" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "wlog" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suff" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "without" "loss" "suffices" ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "gen" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "generally" "have" ssrclear ssr_idcomma ssrhpats_nobs ssrwlogfwd ssrhint (* ssr plugin *) +| "under" ssrrwarg (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne (* ssr plugin *) +| "under" ssrrwarg ssrintros_ne "do" ssrhint3arg (* ssr plugin *) +| "under" ssrrwarg "do" ssrhint3arg (* ssr plugin *) +| "ssrinstancesoftpat" cpattern (* ssrmatching plugin *) +] + +var_list: [ +| var_list var +| var +] + +var_list_opt: [ +| var_list_opt var +| empty +] + +constr_with_bindings_opt: [ +| constr_with_bindings +| empty +] + +int_or_var_opt: [ +| int_or_var +| empty +] + +uconstr_list_opt: [ +| uconstr_list_opt uconstr +| empty +] + +constr_with_bindings_arg_list_comma: [ +| constr_with_bindings_arg_list_comma "," constr_with_bindings_arg +| constr_with_bindings_arg +] + +fixdecl_list: [ +| fixdecl_list fixdecl +| fixdecl +] + +cofixdecl_list: [ +| cofixdecl_list cofixdecl +| cofixdecl +] + +pattern_occ_list_opt: [ +| pattern_occ_list_opt "," pattern_occ as_name +| empty +] + +oriented_rewriter_list_comma: [ +| oriented_rewriter_list_comma "," oriented_rewriter +| oriented_rewriter +] + +simple_alt: [ +| "simple" "inversion" +| "inversion" +| "inversion_clear" +] + +with_opt2: [ +| "with" term +| empty +] + +tactic_opt: [ +| tactic +| empty +] + +reference_opt: [ +| reference +| empty +] + +bindings_list_comma: [ +| bindings_list_comma "," bindings +| bindings +] + +rename_list_comma: [ +| rename_list_comma "," rename +| rename +] + +orient_string: [ +| orient preident +] + +comparison: [ +| "=" +| "<" +| "<=" +| ">" +| ">=" +] + +test: [ +| int_or_var comparison int_or_var +] + +hintbases: [ +| "with" "*" +| "with" preident_list +| empty +] + +preident_list: [ +| preident_list preident +| preident +] + +auto_using: [ +| "using" uconstr_list_comma +| empty +] + +uconstr_list_comma: [ +| uconstr_list_comma "," uconstr +| uconstr +] + +hints_path_atom: [ +| global_list +| "_" +] + +hints_path: [ +| "(" hints_path ")" +| hints_path "*" +| "emp" +| "eps" +| hints_path "|" hints_path +| hints_path_atom +| hints_path hints_path +] + +opthints: [ +| ":" preident_list +| empty +] + +debug: [ +| "debug" +| empty +] + +eauto_search_strategy: [ +| "(bfs)" +| "(dfs)" +| empty +] + +glob_constr_with_bindings: [ +| constr_with_bindings +] + +rewstrategy: [ +| glob +| "<-" term +| "subterms" rewstrategy +| "subterm" rewstrategy +| "innermost" rewstrategy +| "outermost" rewstrategy +| "bottomup" rewstrategy +| "topdown" rewstrategy +| "id" +| "fail" +| "refl" +| "progress" rewstrategy +| "try" rewstrategy +| "any" rewstrategy +| "repeat" rewstrategy +| rewstrategy ";" rewstrategy +| "(" rewstrategy ")" +| "choice" rewstrategy rewstrategy +| "old_hints" preident +| "hints" preident +| "terms" term_list_opt +| "eval" red_expr +| "fold" term +] + +term_list_opt: [ +| term_list_opt term +| empty +] + +int_or_var: [ +| integer +| ident +] + +nat_or_var: [ +| natural +| ident +] + +id_or_meta: [ +| ident +] + +open_constr: [ +| term +] + +uconstr: [ +| term +] + +destruction_arg: [ +| natural +| constr_with_bindings +| constr_with_bindings_arg +] + +constr_with_bindings_arg: [ +| ">" constr_with_bindings +| constr_with_bindings +] + +quantified_hypothesis: [ +| ident +| natural +] + +conversion: [ +| term +| term "with" term +| term "at" occs_nums "with" term +] + +occs_nums: [ +| nat_or_var_list +| "-" nat_or_var int_or_var_list_opt +] + +nat_or_var_list: [ +| nat_or_var_list nat_or_var +| nat_or_var +] + +int_or_var_list_opt: [ +| int_or_var_list_opt int_or_var +| empty +] + +occs: [ +| "at" occs_nums +| empty +] + +pattern_occ: [ +| term occs +] + +ref_or_pattern_occ: [ +| smart_global occs +| term occs +] + +unfold_occ: [ +| smart_global occs +] + +intropattern_list_opt: [ +| intropattern_list_opt intropattern +| empty +] + +or_and_intropattern: [ +| "[" intropattern_or_list_or "]" +| "(" simple_intropattern_list_comma_opt ")" +| "(" simple_intropattern "&" simple_intropattern_list_ ")" +] + +simple_intropattern_list_comma_opt: [ +| simple_intropattern_list_comma +| empty +] + +simple_intropattern_list_comma: [ +| simple_intropattern_list_comma "," simple_intropattern +| simple_intropattern +] + +simple_intropattern_list_: [ +| simple_intropattern_list_ "&" simple_intropattern +| simple_intropattern +] + +intropattern_or_list_or: [ +| intropattern_or_list_or "|" intropattern_list_opt +| intropattern_list_opt +] + +simple_intropattern_list_opt: [ +| simple_intropattern_list_opt simple_intropattern +| empty +] + +equality_intropattern: [ +| "->" +| "<-" +| "[=" intropattern_list_opt "]" +] + +naming_intropattern: [ +| "?" ident +| "?" +| ident +] + +intropattern: [ +| simple_intropattern +| "*" +| "**" +] + +simple_intropattern: [ +| simple_intropattern_closed operconstr0_list_opt +] + +operconstr0_list_opt: [ +| operconstr0_list_opt "%" operconstr0 +| empty +] + +simple_intropattern_closed: [ +| or_and_intropattern +| equality_intropattern +| "_" +| naming_intropattern +] + +simple_binding: [ +| "(" ident ":=" lconstr ")" +| "(" natural ":=" lconstr ")" +] + +bindings: [ +| simple_binding_list +| term_list +] + +simple_binding_list: [ +| simple_binding_list simple_binding +| simple_binding +] + +term_list: [ +| term_list term +| term +] + +constr_with_bindings: [ +| term with_bindings +] + +with_bindings: [ +| "with" bindings +| empty +] + +red_flags: [ +| "beta" +| "iota" +| "match" +| "fix" +| "cofix" +| "zeta" +| "delta" delta_flag +] + +delta_flag: [ +| "-" "[" smart_global_list "]" +| "[" smart_global_list "]" +| empty +] + +smart_global_list: [ +| smart_global_list smart_global +| smart_global +] + +strategy_flag: [ +| red_flags_list +| delta_flag +] + +red_flags_list: [ +| red_flags_list red_flags +| red_flags +] + +red_expr: [ +| "red" +| "hnf" +| "simpl" delta_flag ref_or_pattern_occ_opt +| "cbv" strategy_flag +| "cbn" strategy_flag +| "lazy" strategy_flag +| "compute" delta_flag +| "vm_compute" ref_or_pattern_occ_opt +| "native_compute" ref_or_pattern_occ_opt +| "unfold" unfold_occ_list_comma +| "fold" term_list +| "pattern" pattern_occ_list_comma +| IDENT +] + +ref_or_pattern_occ_opt: [ +| ref_or_pattern_occ +| empty +] + +unfold_occ_list_comma: [ +| unfold_occ_list_comma "," unfold_occ +| unfold_occ +] + +pattern_occ_list_comma: [ +| pattern_occ_list_comma "," pattern_occ +| pattern_occ +] + +hypident: [ +| id_or_meta +| "(" "type" "of" id_or_meta ")" +| "(" "value" "of" id_or_meta ")" +| "(" "type" "of" ident ")" (* ssr plugin *) +| "(" "value" "of" ident ")" (* ssr plugin *) +] + +hypident_occ: [ +| hypident occs +] + +clause_dft_concl: [ +| "in" in_clause +| occs +| empty +] + +clause_dft_all: [ +| "in" in_clause +| empty +] + +opt_clause: [ +| "in" in_clause +| "at" occs_nums +| empty +] + +concl_occ: [ +| "*" occs +| empty +] + +in_hyp_list: [ +| "in" id_or_meta_list +| empty +] + +id_or_meta_list: [ +| id_or_meta_list id_or_meta +| id_or_meta +] + +in_hyp_as: [ +| "in" id_or_meta as_ipat +| empty +] + +simple_binder: [ +| name +| "(" name_list ":" lconstr ")" +] + +fixdecl: [ +| "(" ident simple_binder_list_opt fixannot ":" lconstr ")" +] + +cofixdecl: [ +| "(" ident simple_binder_list_opt ":" lconstr ")" +] + +bindings_with_parameters: [ +| "(" ident simple_binder_list_opt ":=" lconstr ")" +] + +simple_binder_list_opt: [ +| simple_binder_list_opt simple_binder +| empty +] + +eliminator: [ +| "using" constr_with_bindings +] + +as_ipat: [ +| "as" simple_intropattern +| empty +] + +or_and_intropattern_loc: [ +| or_and_intropattern +| ident +] + +as_or_and_ipat: [ +| "as" or_and_intropattern_loc +| empty +] + +eqn_ipat: [ +| "eqn" ":" naming_intropattern +| "_eqn" ":" naming_intropattern +| "_eqn" +| empty +] + +as_name: [ +| "as" ident +| empty +] + +by_tactic: [ +| "by" ltac_expr3 +| empty +] + +rewriter: [ +| "!" constr_with_bindings_arg +| qmark_alt constr_with_bindings_arg +| natural "!" constr_with_bindings_arg +| natural qmark_alt constr_with_bindings_arg +| natural constr_with_bindings_arg +| constr_with_bindings_arg +] + +qmark_alt: [ +| "?" +| "?" +] + +oriented_rewriter: [ +| orient rewriter +] + +induction_clause: [ +| destruction_arg as_or_and_ipat eqn_ipat opt_clause +] + +induction_clause_list: [ +| induction_clause_list_comma eliminator_opt opt_clause +] + +induction_clause_list_comma: [ +| induction_clause_list_comma "," induction_clause +| induction_clause +] + +eliminator_opt: [ +| eliminator +| empty +] + +ltac_expr: [ +| binder_tactic +| ltac_expr4 +] + +binder_tactic: [ +| "fun" input_fun_list "=>" ltac_expr +| "let" rec_opt let_clause_list "in" ltac_expr +| "info" ltac_expr +] + +input_fun_list: [ +| input_fun_list input_fun +| input_fun +] + +input_fun: [ +| "_" +| ident +] + +rec_opt: [ +| "rec" +| empty +] + +let_clause_list: [ +| let_clause_list "with" let_clause +| let_clause +] + +let_clause: [ +| ident ":=" ltac_expr +| "_" ":=" ltac_expr +| ident input_fun_list ":=" ltac_expr +] + +ltac_expr4: [ +| ltac_expr3 ";" binder_tactic +| ltac_expr3 ";" ltac_expr3 +| ltac_expr3 ";" "[" gt_opt tactic_then_gen "]" +| ltac_expr3 +| ltac_expr ";" "first" ssr_first_else (* ssr plugin *) +| ltac_expr ";" "first" ssrseqarg (* ssr plugin *) +| ltac_expr ";" "last" ssrseqarg (* ssr plugin *) +] + +gt_opt: [ +| ">" +| empty +] + +tactic_then_gen: [ +| ltac_expr_opt "|" tactic_then_gen +| ltac_expr_opt ".." or_opt ltac_expr_list2 +| ltac_expr +| empty +] + +ltac_expr_opt: [ +| ltac_expr +| empty +] + +ltac_expr_list_or2_opt: [ +| ltac_expr_list_or2 +| empty +] + +ltac_expr_list_or2: [ +| ltac_expr_list_or2 "|" ltac_expr_opt +| ltac_expr_opt +] + +ltac_expr3: [ +| "try" ltac_expr3 +| "do" int_or_var ltac_expr3 +| "timeout" int_or_var ltac_expr3 +| "time" string_opt ltac_expr3 +| "repeat" ltac_expr3 +| "progress" ltac_expr3 +| "once" ltac_expr3 +| "exactly_once" ltac_expr3 +| "infoH" ltac_expr3 +| "abstract" ltac_expr2 +| "abstract" ltac_expr2 "using" ident +| selector ltac_expr3 +| "do" ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "do" ssrortacarg ssrclauses (* ssr plugin *) +| "do" int_or_var ssrmmod ssrdotac ssrclauses (* ssr plugin *) +| "abstract" ssrdgens (* ssr plugin *) +| ltac_expr2 +] + +tactic_mode: [ +| toplevel_selector_opt query_command +| toplevel_selector_opt "{" +| toplevel_selector_opt ltac_info_opt tactic ltac_use_default +| "par" ":" ltac_info_opt tactic ltac_use_default +] + +toplevel_selector_opt: [ +| toplevel_selector +| empty +] + +toplevel_selector: [ +| selector_body ":" +| "!" ":" +| "all" ":" +] + +selector: [ +| "only" selector_body ":" +] + +selector_body: [ +| range_selector_list_comma +| "[" ident "]" +] + +range_selector_list_comma: [ +| range_selector_list_comma "," range_selector +| range_selector +] + +range_selector: [ +| natural "-" natural +| natural +] + +ltac_expr2: [ +| ltac_expr1 "+" binder_tactic +| ltac_expr1 "+" ltac_expr2 +| "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2 +| ltac_expr1 "||" binder_tactic +| ltac_expr1 "||" ltac_expr2 +| ltac_expr1 +] + +ltac_expr1: [ +| match_key reverse_opt "goal" "with" match_context_list "end" +| match_key ltac_expr "with" match_list "end" +| "first" "[" ltac_expr_list_or_opt "]" +| "solve" "[" ltac_expr_list_or_opt "]" +| "idtac" message_token_list_opt +| failkw int_or_var_opt message_token_list_opt +| simple_tactic +| tactic_arg +| reference tactic_arg_compat_list_opt +| ltac_expr ssrintros_ne (* ssr plugin *) +| ltac_expr0 +] + +match_key: [ +| "match" +| "lazymatch" +| "multimatch" +] + +reverse_opt: [ +| "reverse" +| empty +] + +ltac_expr_list_or_opt: [ +| ltac_expr_list_or +| empty +] + +ltac_expr_list_or: [ +| ltac_expr_list_or "|" ltac_expr +| ltac_expr +] + +match_context_list: [ +| or_opt match_context_rule_list_or +] + +match_context_rule_list_or: [ +| match_context_rule_list_or "|" match_context_rule +| match_context_rule +] + +or_opt: [ +| "|" +| empty +] + +eqn_list_or_opt: [ +| eqn_list_or +| empty +] + +eqn_list_or: [ +| eqn_list_or "|" eqn +| eqn +] + +match_context_rule: [ +| match_hyps_list_comma_opt "|-" match_pattern "=>" ltac_expr +| "[" match_hyps_list_comma_opt "|-" match_pattern "]" "=>" ltac_expr +| "_" "=>" ltac_expr +] + +match_hyps_list_comma_opt: [ +| match_hyps_list_comma +| empty +] + +match_hyps_list_comma: [ +| match_hyps_list_comma "," match_hyps +| match_hyps +] + +match_hyps: [ +| name ":" match_pattern +| name ":=" match_pattern_opt match_pattern +] + +match_pattern: [ +| "context" ident_opt "[" lconstr_pattern "]" +| lconstr_pattern +] + +ident_opt: [ +| ident +| empty +] + +lconstr_pattern: [ +| lconstr +] + +match_pattern_opt: [ +| "[" match_pattern "]" ":" +| empty +] + +match_list: [ +| or_opt match_rule_list_or +] + +match_rule_list_or: [ +| match_rule_list_or "|" match_rule +| match_rule +] + +match_rule: [ +| match_pattern "=>" ltac_expr +| "_" "=>" ltac_expr +] + +message_token_list_opt: [ +| message_token_list_opt message_token +| empty +] + +message_token: [ +| ident +| STRING +| integer +] + +failkw: [ +| "fail" +| "gfail" +] + +tactic_arg: [ +| "eval" red_expr "in" term +| "context" ident "[" lconstr "]" +| "type" "of" term +| "fresh" fresh_id_list_opt +| "type_term" uconstr +| "numgoals" +] + +fresh_id_list_opt: [ +| fresh_id_list_opt fresh_id +| empty +] + +fresh_id: [ +| STRING +| qualid +] + +tactic_arg_compat_list_opt: [ +| tactic_arg_compat_list_opt tactic_arg_compat +| empty +] + +tactic_arg_compat: [ +| tactic_arg +| term +| "()" +] + +ltac_expr0: [ +| "(" ltac_expr ")" +| "[" ">" tactic_then_gen "]" +| tactic_atom +| ssrparentacarg (* ssr plugin *) +] + +tactic_atom: [ +| integer +| reference +| "()" +] + +constr_may_eval: [ +| "eval" red_expr "in" term +| "context" ident "[" lconstr "]" +| "type" "of" term +| term +] + +ltac_def_kind: [ +| ":=" +| "::=" +] + +tacdef_body: [ +| global input_fun_list ltac_def_kind ltac_expr +| global ltac_def_kind ltac_expr +] + +tactic: [ +| ltac_expr +] + +ltac_info_opt: [ +| ltac_info +| empty +] + +ltac_info: [ +| "Info" natural +] + +ltac_use_default: [ +| "." +| "..." +] + +ltac_tactic_level: [ +| "(" "at" "level" natural ")" +] + +ltac_production_sep: [ +| "," string +] + +ltac_production_item: [ +| string +| ident "(" ident ltac_production_sep_opt ")" +| ident +] + +ltac_production_sep_opt: [ +| ltac_production_sep +| empty +] + +ltac_tacdef_body: [ +| tacdef_body +] + +firstorder_using: [ +| "using" reference +| "using" reference "," reference_list_comma +| "using" reference reference reference_list_opt +| empty +] + +reference_list_comma: [ +| reference_list_comma "," reference +| reference +] + +numnotoption: [ +| empty +| "(" "warning" "after" bigint ")" +| "(" "abstract" "after" bigint ")" +] + +mlname: [ +| preident (* extraction plugin *) +| string (* extraction plugin *) +] + +int_or_id: [ +| preident (* extraction plugin *) +| integer (* extraction plugin *) +] + +language: [ +| "Ocaml" (* extraction plugin *) +| "OCaml" (* extraction plugin *) +| "Haskell" (* extraction plugin *) +| "Scheme" (* extraction plugin *) +| "JSON" (* extraction plugin *) +] + +fun_ind_using: [ +| "using" constr_with_bindings (* funind plugin *) +| empty (* funind plugin *) +] + +with_names: [ +| "as" simple_intropattern (* funind plugin *) +| empty (* funind plugin *) +] + +constr_comma_sequence': [ +| term "," constr_comma_sequence' (* funind plugin *) +| term (* funind plugin *) +] + +auto_using': [ +| "using" constr_comma_sequence' (* funind plugin *) +| empty (* funind plugin *) +] + +function_rec_definition_loc: [ +| rec_definition (* funind plugin *) +] + +fun_scheme_arg: [ +| ident ":=" "Induction" "for" reference "Sort" sort_family (* funind plugin *) +] + +ring_mod: [ +| "decidable" term (* setoid_ring plugin *) +| "abstract" (* setoid_ring plugin *) +| "morphism" term (* setoid_ring plugin *) +| "constants" "[" tactic "]" (* setoid_ring plugin *) +| "closed" "[" global_list "]" (* setoid_ring plugin *) +| "preprocess" "[" tactic "]" (* setoid_ring plugin *) +| "postprocess" "[" tactic "]" (* setoid_ring plugin *) +| "setoid" term term (* setoid_ring plugin *) +| "sign" term (* setoid_ring plugin *) +| "power" term "[" global_list "]" (* setoid_ring plugin *) +| "power_tac" term "[" tactic "]" (* setoid_ring plugin *) +| "div" term (* setoid_ring plugin *) +] + +ring_mods: [ +| "(" ring_mod_list_comma ")" (* setoid_ring plugin *) +] + +ring_mod_list_comma: [ +| ring_mod_list_comma "," ring_mod +| ring_mod +] + +field_mod: [ +| ring_mod (* setoid_ring plugin *) +| "completeness" term (* setoid_ring plugin *) +] + +field_mods: [ +| "(" field_mod_list_comma ")" (* setoid_ring plugin *) +] + +field_mod_list_comma: [ +| field_mod_list_comma "," field_mod +| field_mod +] + +ssrtacarg: [ +| ltac_expr (* ssr plugin *) +] + +ssrtac3arg: [ +| ltac_expr3 (* ssr plugin *) +] + +ssrtclarg: [ +| ssrtacarg (* ssr plugin *) +] + +ssrhyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_hyp: [ +| ident (* ssr plugin *) +] + +ssrhoi_id: [ +| ident (* ssr plugin *) +] + +ssrsimpl_ne: [ +| "//=" (* ssr plugin *) +| "/=" (* ssr plugin *) +| "/" natural "/" natural "=" (* ssr plugin *) +| "/" natural "/" (* ssr plugin *) +| "/" natural "=" (* ssr plugin *) +| "/" natural "/=" (* ssr plugin *) +| "/" natural "/" "=" (* ssr plugin *) +| "//" natural "=" (* ssr plugin *) +| "//" (* ssr plugin *) +] + +ssrclear_ne: [ +| "{" ssrhyp_list "}" (* ssr plugin *) +] + +ssrclear: [ +| ssrclear_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrindex: [ +| int_or_var (* ssr plugin *) +] + +ssrocc: [ +| natural natural_list_opt (* ssr plugin *) +| "-" natural_list_opt (* ssr plugin *) +| "+" natural_list_opt (* ssr plugin *) +] + +natural_list_opt: [ +| natural_list_opt natural +| empty +] + +ssrmmod: [ +| "!" (* ssr plugin *) +| "?" (* ssr plugin *) +| "?" (* ssr plugin *) +] + +ssrmult_ne: [ +| natural ssrmmod (* ssr plugin *) +| ssrmmod (* ssr plugin *) +] + +ssrmult: [ +| ssrmult_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrdocc: [ +| "{" ssrocc "}" (* ssr plugin *) +| "{" ssrhyp_list_opt "}" (* ssr plugin *) +] + +ssrhyp_list_opt: [ +| ssrhyp_list_opt ssrhyp +| empty +] + +ssrterm: [ +| "YouShouldNotTypeThis" term (* ssr plugin *) +| term (* ssr plugin *) +] + +ast_closure_term: [ +| term (* ssr plugin *) +] + +ast_closure_lterm: [ +| lconstr (* ssr plugin *) +] + +ssrbwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| "/" term (* ssr plugin *) +| "/" term ssrbwdview (* ssr plugin *) +] + +ssrfwdview: [ +| "YouShouldNotTypeThis" (* ssr plugin *) +| "/" ast_closure_term (* ssr plugin *) +| "/" ast_closure_term ssrfwdview (* ssr plugin *) +] + +ident_no_do: [ +| "YouShouldNotTypeThis" ident (* ssr plugin *) +| IDENT (* ssr plugin *) +] + +ssripat: [ +| "_" (* ssr plugin *) +| "*" (* ssr plugin *) +| ">" (* ssr plugin *) +| ident_no_do (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| "++" (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| ssrdocc (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +| "-" (* ssr plugin *) +| "-/" "=" (* ssr plugin *) +| "-/=" (* ssr plugin *) +| "-/" "/" (* ssr plugin *) +| "-//" (* ssr plugin *) +| "-/" integer "/" (* ssr plugin *) +| "-/" "/=" (* ssr plugin *) +| "-//" "=" (* ssr plugin *) +| "-//=" (* ssr plugin *) +| "-/" integer "/=" (* ssr plugin *) +| "-/" integer "/" integer "=" (* ssr plugin *) +| ssrfwdview (* ssr plugin *) +| "[" ":" ident_list_opt "]" (* ssr plugin *) +| "[:" ident_list_opt "]" (* ssr plugin *) +| ssrcpat (* ssr plugin *) +] + +ident_list_opt: [ +| ident_list_opt ident +| empty +] + +ssripats: [ +| ssripat ssripats (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssriorpat: [ +| ssripats "|" ssriorpat (* ssr plugin *) +| ssripats "|-" ">" ssriorpat (* ssr plugin *) +| ssripats "|-" ssriorpat (* ssr plugin *) +| ssripats "|->" ssriorpat (* ssr plugin *) +| ssripats "||" ssriorpat (* ssr plugin *) +| ssripats "|||" ssriorpat (* ssr plugin *) +| ssripats "||||" ssriorpat (* ssr plugin *) +| ssripats (* ssr plugin *) +] + +ssrcpat: [ +| "YouShouldNotTypeThis" ssriorpat (* ssr plugin *) +| "[" hat "]" (* ssr plugin *) +| "[" ssriorpat "]" (* ssr plugin *) +| "[=" ssriorpat "]" (* ssr plugin *) +] + +hat: [ +| "^" ident (* ssr plugin *) +| "^" "~" ident (* ssr plugin *) +| "^" "~" natural (* ssr plugin *) +| "^~" ident (* ssr plugin *) +| "^~" natural (* ssr plugin *) +] + +ssripats_ne: [ +| ssripat ssripats (* ssr plugin *) +] + +ssrhpats: [ +| ssripats (* ssr plugin *) +] + +ssrhpats_wtransp: [ +| ssripats (* ssr plugin *) +| ssripats "@" ssripats (* ssr plugin *) +] + +ssrhpats_nobs: [ +| ssripats (* ssr plugin *) +] + +ssrrpat: [ +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrintros_ne: [ +| "=>" ssripats_ne (* ssr plugin *) +] + +ssrintros: [ +| ssrintros_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrintrosarg: [ +| "YouShouldNotTypeThis" ssrtacarg ssrintros_ne (* ssr plugin *) +] + +ssrfwdid: [ +| ident (* ssr plugin *) +] + +ssrortacs: [ +| ssrtacarg "|" ssrortacs (* ssr plugin *) +| ssrtacarg "|" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +| "|" ssrortacs (* ssr plugin *) +| "|" (* ssr plugin *) +] + +ssrhintarg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtacarg (* ssr plugin *) +] + +ssrhint3arg: [ +| "[" "]" (* ssr plugin *) +| "[" ssrortacs "]" (* ssr plugin *) +| ssrtac3arg (* ssr plugin *) +] + +ssrortacarg: [ +| "[" ssrortacs "]" (* ssr plugin *) +] + +ssrhint: [ +| empty (* ssr plugin *) +| "by" ssrhintarg (* ssr plugin *) +] + +ssrwgen: [ +| ssrclear_ne (* ssr plugin *) +| ssrhoi_hyp (* ssr plugin *) +| "@" ssrhoi_hyp (* ssr plugin *) +| "(" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" ssrhoi_id ")" (* ssr plugin *) +| "(@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +| "(" "@" ssrhoi_id ":=" lcpattern ")" (* ssr plugin *) +] + +ssrclausehyps: [ +| ssrwgen "," ssrclausehyps (* ssr plugin *) +| ssrwgen ssrclausehyps (* ssr plugin *) +| ssrwgen (* ssr plugin *) +] + +ssrclauses: [ +| "in" ssrclausehyps "|-" "*" (* ssr plugin *) +| "in" ssrclausehyps "|-" (* ssr plugin *) +| "in" ssrclausehyps "*" (* ssr plugin *) +| "in" ssrclausehyps (* ssr plugin *) +| "in" "|-" "*" (* ssr plugin *) +| "in" "*" (* ssr plugin *) +| "in" "*" "|-" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrfwd: [ +| ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrbvar: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +] + +ssrbinder: [ +| ssrbvar (* ssr plugin *) +| "(" ssrbvar ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ssrbvar_list ":" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":" lconstr ":=" lconstr ")" (* ssr plugin *) +| "(" ssrbvar ":=" lconstr ")" (* ssr plugin *) +| of_alt operconstr99 (* ssr plugin *) +] + +ssrbvar_list: [ +| ssrbvar_list ssrbvar +| ssrbvar +] + +ssrstruct: [ +| "{" "struct" ident "}" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrposefwd: [ +| ssrbinder_list_opt ssrfwd (* ssr plugin *) +] + +ssrfixfwd: [ +| "fix" ssrbvar ssrbinder_list_opt ssrstruct ssrfwd (* ssr plugin *) +] + +ssrcofixfwd: [ +| "cofix" ssrbvar ssrbinder_list_opt ssrfwd (* ssr plugin *) +] + +ssrbinder_list_opt: [ +| ssrbinder_list_opt ssrbinder +| empty +] + +ssrsetfwd: [ +| ":" ast_closure_lterm ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":" ast_closure_lterm ":=" lcpattern (* ssr plugin *) +| ":=" "{" ssrocc "}" cpattern (* ssr plugin *) +| ":=" lcpattern (* ssr plugin *) +] + +ssrhavefwd: [ +| ":" ast_closure_lterm ssrhint (* ssr plugin *) +| ":" ast_closure_lterm ":=" ast_closure_lterm (* ssr plugin *) +| ":" ast_closure_lterm ":=" (* ssr plugin *) +| ":=" ast_closure_lterm (* ssr plugin *) +] + +ssrhavefwdwbinders: [ +| ssrhpats_wtransp ssrbinder_list_opt ssrhavefwd (* ssr plugin *) +] + +ssrseqarg: [ +| ssrswap (* ssr plugin *) +| ssrseqidx ssrortacarg ssrorelse_opt (* ssr plugin *) +| ssrseqidx ssrswap (* ssr plugin *) +| ltac_expr3 (* ssr plugin *) +] + +ssrorelse_opt: [ +| ssrorelse +| empty +] + +ssrseqidx: [ +| ident (* ssr plugin *) +| natural (* ssr plugin *) +] + +ssrswap: [ +| "first" (* ssr plugin *) +| "last" (* ssr plugin *) +] + +ssrorelse: [ +| "||" ltac_expr2 (* ssr plugin *) +] + +ident: [ +| IDENT +] + +ssrparentacarg: [ +| "(" ltac_expr ")" (* ssr plugin *) +] + +ssrdotac: [ +| ltac_expr3 (* ssr plugin *) +| ssrortacarg (* ssr plugin *) +] + +ssr_first: [ +| ssr_first ssrintros_ne (* ssr plugin *) +| "[" ltac_expr_list_or_opt "]" (* ssr plugin *) +] + +ssr_first_else: [ +| ssr_first ssrorelse (* ssr plugin *) +| ssr_first (* ssr plugin *) +] + +ssrgen: [ +| ssrdocc cpattern (* ssr plugin *) +| cpattern (* ssr plugin *) +] + +ssrdgens_tl: [ +| "{" ssrhyp_list "}" cpattern ssrdgens_tl (* ssr plugin *) +| "{" ssrhyp_list "}" (* ssr plugin *) +| "{" ssrocc "}" cpattern ssrdgens_tl (* ssr plugin *) +| "/" ssrdgens_tl (* ssr plugin *) +| cpattern ssrdgens_tl (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrdgens: [ +| ":" ssrgen ssrdgens_tl (* ssr plugin *) +] + +ssreqid: [ +| ssreqpat (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssreqpat: [ +| ident (* ssr plugin *) +| "_" (* ssr plugin *) +| "?" (* ssr plugin *) +| "+" (* ssr plugin *) +| ssrdocc "->" (* ssr plugin *) +| ssrdocc "<-" (* ssr plugin *) +| "->" (* ssr plugin *) +| "<-" (* ssr plugin *) +] + +ssrarg: [ +| ssrfwdview ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrfwdview ssrclear ssrintros (* ssr plugin *) +| ssreqid ssrdgens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +] + +ssrmovearg: [ +| ssrarg (* ssr plugin *) +] + +ssrcasearg: [ +| ssrarg (* ssr plugin *) +] + +ssragen: [ +| "{" ssrhyp_list "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrhyp_list: [ +| ssrhyp_list ssrhyp +| ssrhyp +] + +ssragens: [ +| "{" ssrhyp_list "}" ssrterm ssragens (* ssr plugin *) +| "{" ssrhyp_list "}" (* ssr plugin *) +| ssrterm ssragens (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrapplyarg: [ +| ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrclear_ne ssrintros (* ssr plugin *) +| ssrintros_ne (* ssr plugin *) +| ssrbwdview ":" ssragen ssragens ssrintros (* ssr plugin *) +| ssrbwdview ssrclear ssrintros (* ssr plugin *) +] + +ssrexactarg: [ +| ":" ssragen ssragens (* ssr plugin *) +| ssrbwdview ssrclear (* ssr plugin *) +| ssrclear_ne (* ssr plugin *) +] + +ssrcongrarg: [ +| natural term ssrdgens (* ssr plugin *) +| natural term (* ssr plugin *) +| term ssrdgens (* ssr plugin *) +| term (* ssr plugin *) +] + +ssrrwocc: [ +| "{" ssrhyp_list_opt "}" (* ssr plugin *) +| "{" ssrocc "}" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrrule_ne: [ +| ssrterm_alt (* ssr plugin *) +| ssrsimpl_ne (* ssr plugin *) +] + +ssrterm_alt: [ +| "/" ssrterm +| ssrterm +| ssrsimpl_ne +] + +ssrrule: [ +| ssrrule_ne (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrpattern_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrpattern_ne_squarep: [ +| "[" rpattern "]" (* ssr plugin *) +] + +ssrrwarg: [ +| "-" ssrmult ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "-/" ssrterm (* ssr plugin *) +| ssrmult_ne ssrrwocc ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" ssrhyp_list "}" ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| "{" ssrhyp_list "}" ssrrule (* ssr plugin *) +| "{" ssrocc "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| "{" "}" ssrpattern_squarep ssrrule_ne (* ssr plugin *) +| ssrpattern_ne_squarep ssrrule_ne (* ssr plugin *) +| ssrrule_ne (* ssr plugin *) +] + +ssrrwargs: [ +| ssrrwarg_list (* ssr plugin *) +] + +ssrrwarg_list: [ +| ssrrwarg_list ssrrwarg +| ssrrwarg +] + +ssrunlockarg: [ +| "{" ssrocc "}" ssrterm (* ssr plugin *) +| ssrterm (* ssr plugin *) +] + +ssrunlockargs: [ +| ssrunlockarg_list_opt (* ssr plugin *) +] + +ssrunlockarg_list_opt: [ +| ssrunlockarg_list_opt ssrunlockarg +| empty +] + +ssrsufffwd: [ +| ssrhpats ssrbinder_list_opt ":" ast_closure_lterm ssrhint (* ssr plugin *) +] + +ssrwlogfwd: [ +| ":" ssrwgen_list_opt "/" ast_closure_lterm (* ssr plugin *) +] + +ssrwgen_list_opt: [ +| ssrwgen_list_opt ssrwgen +| empty +] + +ssr_idcomma: [ +| empty (* ssr plugin *) +| IDENT_alt "," (* ssr plugin *) +] + +IDENT_alt: [ +| IDENT +| "_" +] + +ssr_rtype: [ +| "return" operconstr100 (* ssr plugin *) +] + +ssr_mpat: [ +| pattern200 (* ssr plugin *) +] + +ssr_dpat: [ +| ssr_mpat "in" pattern200 ssr_rtype (* ssr plugin *) +| ssr_mpat ssr_rtype (* ssr plugin *) +| ssr_mpat (* ssr plugin *) +] + +ssr_dthen: [ +| ssr_dpat "then" lconstr (* ssr plugin *) +] + +ssr_elsepat: [ +| "else" (* ssr plugin *) +] + +ssr_else: [ +| ssr_elsepat lconstr (* ssr plugin *) +] + +ssr_search_item: [ +| string (* ssr plugin *) +| string "%" preident (* ssr plugin *) +| constr_pattern (* ssr plugin *) +] + +ssr_search_arg: [ +| "-" ssr_search_item ssr_search_arg (* ssr plugin *) +| ssr_search_item ssr_search_arg (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssr_modlocs: [ +| empty (* ssr plugin *) +| "in" modloc_list (* ssr plugin *) +] + +modloc_list: [ +| modloc_list modloc +| modloc +] + +modloc: [ +| "-" global (* ssr plugin *) +| global (* ssr plugin *) +] + +ssrhintref: [ +| term (* ssr plugin *) +| term "|" natural (* ssr plugin *) +] + +ssrviewpos: [ +| "for" "move" "/" (* ssr plugin *) +| "for" "apply" "/" (* ssr plugin *) +| "for" "apply" "/" "/" (* ssr plugin *) +| "for" "apply" "//" (* ssr plugin *) +| empty (* ssr plugin *) +] + +ssrviewposspc: [ +| ssrviewpos (* ssr plugin *) +] + +rpattern: [ +| lconstr (* ssrmatching plugin *) +| "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr (* ssrmatching plugin *) +| "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "in" lconstr "in" lconstr (* ssrmatching plugin *) +| lconstr "as" lconstr "in" lconstr (* ssrmatching plugin *) +] + +cpattern: [ +| "Qed" term (* ssrmatching plugin *) +| term (* ssrmatching plugin *) +] + +lcpattern: [ +| "Qed" lconstr (* ssrmatching plugin *) +| lconstr (* ssrmatching plugin *) +] + +ssrpatternarg: [ +| rpattern (* ssrmatching plugin *) +] + +empty: [ +| +] + +lpar_id_coloneq: [ +| "(" IDENT; ":=" +] + +name_colon: [ +| IDENT; ":" +| "_" ":" +] + +int: [ +| integer +] + +command_entry: [ +| noedit_mode +] + diff --git a/doc/tools/docgram/prodn.edit_mlg b/doc/tools/docgram/prodn.edit_mlg new file mode 100644 index 0000000000..a28d07636a --- /dev/null +++ b/doc/tools/docgram/prodn.edit_mlg @@ -0,0 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Defines additional productions and edits for use in documentation. Not compiled into Coq *) +(* Contents used to generate prodn in doc *) + +DOC_GRAMMAR diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg new file mode 100644 index 0000000000..84acd07075 --- /dev/null +++ b/doc/tools/docgram/productionlist.edit_mlg @@ -0,0 +1,25 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Defines additional productions and edits for use in documentation. Not compiled into Coq *) +(* Contents used to generate productionlists in doc *) + +DOC_GRAMMAR + +EXPAND: [ | ] + +(* ugh todo: try to handle before expansion *) +tactic_then_gen : [ +| REPLACE ltac_expr_opt ".." ltac_expr_opt2 +| WITH ltac_expr_opt ".." or_opt ltac_expr_list2 +] + +ltac_expr_opt2 : [ | DELETENT ] +ltac_expr_list2_opt : [ | DELETENT ] |