diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 42 | ||||
| -rw-r--r-- | doc/sphinx/language/core/variants.rst | 15 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/evars.rst | 32 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/implicit-arguments.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 17 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 100 |
11 files changed, 199 insertions, 76 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 41b726b069..ce68274036 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -99,12 +99,15 @@ Extraction Options Setting the target language ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Extraction Language {| OCaml | Haskell | Scheme } +.. cmd:: Extraction Language {| OCaml | Haskell | Scheme | JSON } :name: Extraction Language The ability to fix target language is the first and more important of the extraction options. Default is ``OCaml``. + The JSON output is mostly for development or debugging: + it contains the raw ML term produced as an intermediary target. + Inlining and optimizations ~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index f9d24fde0e..c27eb216e8 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -40,7 +40,7 @@ in the |Coq| root directory; this includes the modules ``Datatypes``, ``Specif``, ``Peano``, -``Wf`` and +``Wf`` and ``Tactics``. Module ``Logic_Type`` also makes it in the initial state. @@ -175,7 +175,7 @@ Quantifiers Then we find first-order quantifiers: .. coqtop:: in - + Definition all (A:Set) (P:A -> Prop) := forall x:A, P x. Inductive ex (A: Set) (P:A -> Prop) : Prop := ex_intro (x:A) (_:P x). @@ -256,12 +256,12 @@ Finally, a few easy lemmas are provided. single: f_equal2 ... f_equal5 (term) The theorem ``f_equal`` is extended to functions with two to five -arguments. The theorem are names ``f_equal2``, ``f_equal3``, +arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. .. coqtop:: in abort - + Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), @@ -324,7 +324,7 @@ Programming Note that zero is the letter ``O``, and *not* the numeral ``0``. -The predicate ``identity`` is logically +The predicate ``identity`` is logically equivalent to equality but it lives in sort ``Type``. It is mainly maintained for compatibility. @@ -367,7 +367,7 @@ infix notation ``||``), ``xorb``, ``implb`` and ``negb``. Specification ~~~~~~~~~~~~~ -The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. +The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. They are available with the syntax shown in the previous section :ref:`datatypes`. For instance, given :g:`A:Type` and :g:`P:A->Prop`, the construct @@ -393,11 +393,11 @@ provided. .. coqtop:: in Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x). - Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := + Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := exist2 (x:A) (_:P x) (_:Q x). A *strong (dependent) sum* :g:`{x:A & P x}` may be also defined, -when the predicate ``P`` is now defined as a +when the predicate ``P`` is now defined as a constructor of types in ``Type``. .. index:: @@ -556,7 +556,7 @@ section :tacn:`refine`). This scope is opened by default. Now comes the content of module ``Peano``: .. coqdoc:: - + Theorem eq_S : forall x y:nat, x = y -> S x = S y. Definition pred (n:nat) : nat := match n with @@ -628,7 +628,7 @@ induction principle. .. coqdoc:: Theorem nat_case : - forall (n:nat) (P:nat -> Prop), + forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. Theorem nat_double_ind : forall R:nat -> nat -> Prop, @@ -640,7 +640,7 @@ induction principle. Well-founded recursion ~~~~~~~~~~~~~~~~~~~~~~ -The basic library contains the basics of well-founded recursion and +The basic library contains the basics of well-founded recursion and well-founded induction, in module ``Wf.v``. .. index:: @@ -669,7 +669,7 @@ well-founded induction, in module ``Wf.v``. forall P:A -> Prop, (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. -The automatically generated scheme ``Acc_rect`` +The automatically generated scheme ``Acc_rect`` can be used to define functions by fixpoints using well-founded relations to justify termination. Assuming extensionality of the functional used for the recursive call, the @@ -741,7 +741,7 @@ The standard library Survey ~~~~~~ -The rest of the standard library is structured into the following +The rest of the standard library is structured into the following subdirectories: * **Logic** : Classical logic and dependent equality @@ -751,8 +751,8 @@ subdirectories: * **ZArith** : Basic relative integer arithmetic * **Numbers** : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words) * **Bool** : Booleans (basic functions and results) - * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) - * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) + * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) + * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees) * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...) * **Floats** : Machine implementation of floating-point arithmetic (for the binary64 format) @@ -903,7 +903,7 @@ tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: discrR :name: discrR - + Proves that two real integer constants are different. .. example:: @@ -931,7 +931,7 @@ tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: split_Rmult :name: split_Rmult - + Splits a condition that a product is non null into subgoals corresponding to the condition on each operand of the product. @@ -963,7 +963,7 @@ List library single: fold_left (term) single: fold_right (term) -Some elementary operations on polymorphic lists are defined here. +Some elementary operations on polymorphic lists are defined here. They can be accessed by requiring module ``List``. It defines the following notions: @@ -1052,9 +1052,9 @@ Notation Interpretation ``_ + _`` ``add`` ``_ * _`` ``mul`` ``_ / _`` ``div`` -``_ == _`` ``eqb`` -``_ < _`` ``ltb`` -``_ <= _`` ``leb`` +``_ =? _`` ``eqb`` +``_ <? _`` ``ltb`` +``_ <=? _`` ``leb`` ``_ ?= _`` ``compare`` =========== ============== diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index d00a2f4100..8e2bf32dd6 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -57,6 +57,11 @@ Private (matching) inductive types Definition by cases: match -------------------------- +Objects of inductive types can be destructured by a case-analysis +construction called *pattern matching* expression. A pattern matching +expression is used to analyze the structure of an inductive object and +to apply specific treatments accordingly. + .. insertprodn term_match pattern0 .. prodn:: @@ -77,10 +82,12 @@ Definition by cases: match | @numeral | @string -Objects of inductive types can be destructured by a case-analysis -construction called *pattern matching* expression. A pattern matching -expression is used to analyze the structure of an inductive object and -to apply specific treatments accordingly. +Note that the :n:`@pattern ::= @pattern10 : @term` production +is not supported in :n:`match` patterns. Trying to use it will give this error: + +.. exn:: Casts are not supported in this pattern. + :undocumented: + This paragraph describes the basic form of pattern matching. See Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index 40e0898871..20f4310d13 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -13,13 +13,13 @@ Existential variables | ?[ ?@ident ] | ?@ident {? @%{ {+; @ident := @term } %} } -|Coq| terms can include existential variables which represents unknown -subterms to eventually be replaced by actual subterms. +|Coq| terms can include existential variables that represent unknown +subterms that are eventually replaced with actual subterms. -Existential variables are generated in place of unsolvable implicit +Existential variables are generated in place of unsolved implicit arguments or “_” placeholders when using commands such as ``Check`` (see Section :ref:`requests-to-the-environment`) or when using tactics such as -:tacn:`refine`, as well as in place of unsolvable instances when using +:tacn:`refine`, as well as in place of unsolved instances when using tactics such that :tacn:`eapply`. An existential variable is defined in a context, which is the context of variables of the placeholder which generated the existential variable, and a type, @@ -43,22 +43,18 @@ existential variable is represented by “?” followed by an identifier. Check identity _ (fun x => _). In the general case, when an existential variable :n:`?@ident` appears -outside of its context of definition, its instance, written under the -form :n:`{ {*; @ident := @term} }` is appending to its name, indicating +outside its context of definition, its instance, written in the +form :n:`{ {*; @ident := @term} }`, is appended to its name, indicating how the variables of its defining context are instantiated. -The variables of the context of the existential variables which are -instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag -is on (see Section :ref:`explicit-display-existentials`), and this is why an -existential variable used in the same context as its context of definition is written with no instance. +Only the variables that are defined in another context are displayed: +this is why an existential variable used in the same context as its +context of definition is written with no instance. +This behaviour may be changed: see :ref:`explicit-display-existentials`. .. coqtop:: all Check (fun x y => _) 0 1. - Set Printing Existential Instances. - - Check (fun x y => _) 0 1. - Existential variables can be named by the user upon creation using the syntax :n:`?[@ident]`. This is useful when the existential variable needs to be explicitly handled later in the script (e.g. @@ -88,6 +84,14 @@ Explicit displaying of existential instances for pretty-printing context of an existential variable is instantiated at each of the occurrences of the existential variable. +.. coqtop:: all + + Check (fun x y => _) 0 1. + + Set Printing Existential Instances. + + Check (fun x y => _) 0 1. + .. _tactics-in-terms: Solving existential variables using tactics diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index bbd486e3ba..ca69072cb9 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -70,7 +70,7 @@ is said *contextual* if it can be inferred only from the knowledge of the type of the context of the current expression. For instance, the only argument of:: - nil : forall A:Set, list A` + nil : forall A:Set, list A is contextual. Similarly, both arguments of a term of type:: @@ -539,7 +539,7 @@ with free variables into a closed statement where these variables are quantified explicitly. Use the :cmd:`Generalizable` command to designate which variables should be generalized. -It is activated for a binder by prefixing a \`, and for terms by +It is activated within a binder by prefixing it with \`, and for terms by surrounding it with \`{ }, or \`[ ] or \`( ). Terms surrounded by \`{ } introduce their free variables as maximally diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index b4558ef07f..d6a828521f 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -94,7 +94,7 @@ The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1` performs case analysis on :n:`@term__0` whose type must be an inductive type with exactly one constructor. The number of variables :n:`@ident__i` must correspond to the number of arguments of this -contrustor. Then, in :n:`@term__1`, these variables are bound to the +constructor. Then, in :n:`@term__1`, these variables are bound to the arguments of the constructor in :n:`@term__0`. For instance, the definition diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 058b8ccd5c..ec182ce08f 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -81,8 +81,7 @@ loading of the resource file with the option ``-q``. By environment variables ~~~~~~~~~~~~~~~~~~~~~~~~~ -Load path can be specified to the |Coq| system by setting up ``$COQPATH`` -environment variable. It is a list of directories separated by +``$COQPATH`` can be used to specify the load path. It is a list of directories separated by ``:`` (``;`` on Windows). |Coq| will also honor ``$XDG_DATA_HOME`` and ``$XDG_DATA_DIRS`` (see Section :ref:`libraries-and-filesystem`). @@ -92,7 +91,7 @@ not set, they look for the commands in the executable path. .. _COQ_COLORS: -The ``$COQ_COLORS`` environment variable can be used to specify the set +``$COQ_COLORS`` can be used to specify the set of colors used by ``coqtop`` to highlight its output. It uses the same syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated list of assignments of the form :n:`name={*; attr}` where @@ -108,6 +107,22 @@ sets the highlights for added text in diffs to underlined (the 4) with a backgro color (0, 0, 240) and for removed text in diffs to a red background. Note that if you specify ``COQ_COLORS``, the predefined attributes are ignored. +.. _OCAMLRUNPARAM: + +``$OCAMLRUNPARAM``, described +`here <https://caml.inria.fr/pub/docs/manual-ocaml/runtime.html#s:ocamlrun-options>`_, +can be used to specify certain runtime and memory usage parameters. In most cases, +experimenting with these settings will likely not cause a significant performance difference +and should be harmless. + +If the variable is not set, |Coq| uses the +`default values <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEcontrol>`_, +except that ``space_overhead`` is set to 120 and ``minor_heap_size`` is set to 32Mwords +(256MB with 64-bit executables or 128MB with 32-bit executables). + +.. todo: Using the same text "here" for both of the links in the last 2 paragraphs generates + an incorrect warning: coq-commands.rst:4: WARNING: Duplicate explicit target name: "here". + The warning doesn't even have the right line number. :-( .. _command-line-options: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 00aafe1266..4480b10319 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -858,19 +858,28 @@ Controlling the effect of proof editing commands Controlling memory usage ------------------------ +.. cmd:: Print Debug GC + + Prints heap usage statistics, which are values from the `stat` type of the `Gc` module + described + `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_ + in the OCaml documentation. + The `live_words`, `heap_words` and `top_heap_words` values give the basic information. + Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables. + When experiencing high memory usage the following commands can be used to force |Coq| to optimize some of its internal data structures. - .. cmd:: Optimize Proof - This command forces |Coq| to shrink the data structure used to represent - the ongoing proof. + Shrink the data structure used to represent the current proof. .. cmd:: Optimize Heap - This command forces the |OCaml| runtime to perform a heap compaction. - This is in general an expensive operation. - See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ + Perform a heap compaction. This is generally an expensive operation. + See: `OCaml Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ There is also an analogous tactic :tacn:`optimize_heap`. + +Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>` +environment variable. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 7b3670164b..4eaca8634f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1211,6 +1211,8 @@ The move tactic. :tacn:`revert`, :tacn:`rename`, :tacn:`clear` and :tacn:`pattern` tactics. +.. _the_case_tactic_ssr: + The case tactic ``````````````` @@ -1235,7 +1237,17 @@ The case tactic x = 1 -> y = 2 -> G. - Note also that the case of |SSR| performs :g:`False` elimination, even + The :tacn:`case` can generate the following warning: + + .. warn:: SSReflect: cannot obtain new equations out of ... + + The tactic was run on an equation that cannot generate simpler equations, + for example `x = 1`. + + The warning can be silenced or made fatal by using the :opt:`Warnings` option + and the `spurious-ssr-injection` key. + + Finally the :tacn:`case` tactic of |SSR| performs :g:`False` elimination, even if no branch is generated by this case operation. Hence the tactic :tacn:`case` on a goal of the form :g:`False -> G` will succeed and prove the goal. @@ -2280,7 +2292,7 @@ to the others. Iteration ~~~~~~~~~ -.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] } +.. tacn:: do {? @mult } {| @tactic | [ {+| @tactic } ] } :name: do (ssreflect) This tactical offers an accurate control on the repetition of tactics. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 25c4de7389..8635add0e1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2227,9 +2227,6 @@ and an explanation of the underlying technique. then :n:`injection @ident` first introduces the hypothesis in the local context using :n:`intros until @ident`. - .. exn:: Not a projectable equality but a discriminable one. - :undocumented: - .. exn:: Nothing to do, it is an equality between convertible terms. :undocumented: @@ -2237,7 +2234,8 @@ and an explanation of the underlying technique. :undocumented: .. exn:: Nothing to inject. - :undocumented: + + This error is given when one side of the equality is not a constructor. .. tacv:: injection @num @@ -2821,19 +2819,12 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. only in the conclusion of the goal. The clause argument must not contain any ``type of`` nor ``value of``. - .. tacv:: cutrewrite <- (@term = @term’) + .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident } :name: cutrewrite .. deprecated:: 8.5 - This tactic can be replaced by :n:`enough (@term = @term’) as <-`. - - .. tacv:: cutrewrite -> (@term = @term’) - - .. deprecated:: 8.5 - - This tactic can be replaced by :n:`enough (@term = @term’) as ->`. - + Use :tacn:`replace` instead. .. tacn:: subst @ident :name: subst diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 18149a690a..9e8e5e5fa5 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -425,16 +425,98 @@ Displaying information about notations (corresponding to :token:`ltac_expr` in the documentation). - `vernac` - for :token:`command`\s - The first three of these give the precedence and associativity for each construct. - For example, these lines printed by `Print Grammar tactic` indicates that the `try` construct - is at level 3 and right-associative. `SELF` represents the `tactic_expr` nonterminal - at level 5 (the top level):: - + This command doesn't display all nonterminals of the grammar. For example, + productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` + and `tactic_then_gen` which are not shown and can't be printed. + + The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify + what part of the grammar a nonterminal is from. If you examine nonterminal definitions + in the source code, they are identified only by the name following the colon. + + Most of the grammar in the documentation was updated in 8.12 to make it accurate and + readable. This was done using a new developer tool that extracts the grammar from the + source code, edits it and inserts it into the documentation files. While the + edited grammar is equivalent to the original, for readability some nonterminals + have been renamed and others have been eliminated by substituting the nonterminal + definition where the nonterminal was referenced. This command shows the original grammar, + so it won't exactly match the documentation. + + The |Coq| parser is based on Camlp5. The documentation for + `Extensible grammars <http://camlp5.github.io/doc/htmlc/grammars.html>`_ is the + most relevant but it assumes considerable knowledge. Here are the essentials: + + Productions can contain the following elements: + + - nonterminal names - identifiers in the form `[a-zA-Z0-9_]*` + - `"…"` - a literal string that becomes a keyword and cannot be used as an :token:`ident`. + The string doesn't have to be a valid identifier; frequently the string will contain only + punctuation characters. + - `IDENT "…"` - a literal string that has the form of an :token:`ident` + - `OPT element` - optionally include `element` (e.g. a nonterminal, IDENT "…" or "…") + - `LIST1 element` - a list of one or more `element`\s + - `LIST0 element` - an optional list of `element`\s + - `LIST1 element SEP sep` - a list of `element`\s separated by `sep` + - `LIST0 element SEP sep` - an optional list of `element`\s separated by `sep` + - `[ elements1 | elements2 | … ]` - alternatives (either `elements1` or `elements2` or …) + + Nonterminals can have multiple **levels** to specify precedence and associativity + of its productions. This feature of grammars makes it simple to parse input + such as `1+2*3` in the usual way as `1+(2*3)`. However, most nonterminals have a single level. + + For example, this output from `Print Grammar tactic` shows the first 3 levels for + `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative, + which applies to the productions within it, such as the `try` construct:: + + Entry tactic:tactic_expr is + [ "5" RIGHTA + [ tactic:binder_tactic ] + | "4" LEFTA + [ SELF; ";"; tactic:binder_tactic + | SELF; ";"; SELF + | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] | "3" RIGHTA [ IDENT "try"; SELF + : + + The interpretation of `SELF` depends on its position in the production and the + associativity of the level: + + - At the beginning of a production, `SELF` means the next level. In the + fragment shown above, the next level for `try` is "2". (This is defined by the order + of appearance in the grammar or output; the levels could just as well be + named "foo" and "bar".) + - In the middle of a production, `SELF` means the top level ("5" in the fragment) + - At the end of a production, `SELF` means the next level within + `LEFTA` levels and the current level within `RIGHTA` levels. + + `NEXT` always means the next level. `nonterminal LEVEL "…"` is a reference to the specified level + for `nonterminal`. + + `Associativity <http://camlp5.github.io/doc/htmlc/grammars.html#b:Associativity>`_ + explains `SELF` and `NEXT` in somewhat more detail. + + The output for `Print Grammar constr` includes :cmd:`Notation` definitions, + which are dynamically added to the grammar at run time. + For example, in the definition for `operconstr`, the production on the second line shown + here is defined by a :cmd:`Reserved Notation` command in `Notations.v`:: + + | "50" LEFTA + [ SELF; "||"; NEXT + + Similarly, `Print Grammar tactic` includes :cmd:`Tactic Notation`\s, such as :tacn:`dintuition`. + + The file + `doc/tools/docgram/fullGrammar <http://github.com/coq/coq/blob/master/doc/tools/docgram/fullGrammar>`_ + in the source tree extracts the full grammar for + |Coq| (not including notations and tactic notations defined in `*.v` files nor some optionally-loaded plugins) + in a single file with minor changes to handle nonterminals using multiple levels (described in + `doc/tools/docgram/README.md <http://github.com/coq/coq/blob/master/doc/tools/docgram/README.md>`_). + This is complete and much easier to read than the grammar source files. + `doc/tools/docgram/orderedGrammar <http://github.com/coq/coq/blob/master/doc/tools/docgram/orderedGrammar>`_ + has the edited grammar that's used in the documentation. - Note that the productions printed by this command are represented in the form used by - |Coq|'s parser (coqpp), which differs from how productions are shown in the documentation. + Developer documentation for parsing is in + `dev/doc/parsing.md <http://github.com/coq/coq/blob/master/dev/doc/parsing.md>`_. .. _locating-notations: @@ -872,7 +954,7 @@ where ``x`` is any expression parsed in entry the given rule) and ``y`` is any expression parsed in entry ``expr`` at level strictly less than ``2``. -Rules associated to an entry can refer different sub-entries. The +Rules associated with an entry can refer different sub-entries. The grammar entry name ``constr`` can be used to refer to the main grammar of term as in the rule @@ -958,7 +1040,7 @@ up to the insertion of a pair of curly brackets. .. cmd:: Print Custom Grammar @ident :name: Print Custom Grammar - This displays the state of the grammar for terms associated to + This displays the state of the grammar for terms associated with the custom entry :token:`ident`. .. _NotationSyntax: |