diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/_static/diffs-show-proof.png | bin | 0 -> 13641 bytes | |||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/records.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 38 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 43 |
5 files changed, 62 insertions, 25 deletions
diff --git a/doc/sphinx/_static/diffs-show-proof.png b/doc/sphinx/_static/diffs-show-proof.png Binary files differnew file mode 100644 index 0000000000..62bd9cccd0 --- /dev/null +++ b/doc/sphinx/_static/diffs-show-proof.png diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 4cdfba146a..39b154de8d 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -13,7 +13,7 @@ Inductive types .. prodn:: inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } - | {? @ident } %{ {*; @record_field } %} + | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } This command defines one or more diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index cd44d06e67..b2099b8636 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -18,12 +18,12 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. insertprodn record_definition field_def .. prodn:: - record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations } + record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations } record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations } field_body ::= {* @binder } @of_type | {* @binder } @of_type := @term | {* @binder } := @term - term_record ::= %{%| {* @field_def } %|%} + term_record ::= %{%| {*; @field_def } {? ; } %|%} field_def ::= @qualid {* @binder } := @term diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index f90ebadb3a..f722ddda79 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -590,11 +590,11 @@ Requesting information constructed. Each hole is an existential variable, which appears as a question mark followed by an identifier. - Experimental: Specifying “Diffs” highlights the difference between the + Specifying “Diffs” highlights the difference between the current and previous proof step. By default, the command shows the output once with additions highlighted. Including “removed” shows the output twice: once showing removals and once showing additions. - It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`. + It does not examine the :opt:`Diffs` option. See :ref:`showing_proof_diffs`. .. cmdv:: Show Conjectures :name: Show Conjectures @@ -675,12 +675,9 @@ Requesting information Showing differences between proof steps --------------------------------------- - Coq can automatically highlight the differences between successive proof steps -and between values in some error messages. Also, as an experimental feature, -Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` -command, but only, for now, when using coqtop and Proof General. - +and between values in some error messages. Coq can also highlight differences +in the proof term. For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added @@ -826,14 +823,37 @@ the split because it has not changed. .. image:: ../_static/diffs-coqide-multigoal.png :alt: coqide with Set Diffs on with multiple goals -This is how diffs may appear after applying a :tacn:`intro` tactic that results -in compacted hypotheses: +Diffs may appear like this after applying a :tacn:`intro` tactic that results +in a compacted hypotheses: .. .. image:: ../_static/diffs-coqide-compacted.png :alt: coqide with Set Diffs on with compacted hypotheses +.. _showing_proof_diffs: + +"Show Proof" differences +```````````````````````` + +To show differences in the proof term: + +- In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command. + +- In CoqIDE, position the cursor on or just after a tactic to compare the proof term + after the tactic with the proof term before the tactic, then select + `View / Show Proof` from the menu or enter the associated key binding. + Differences will be shown applying the current `Show Diffs` setting + from the `View` menu. If the current setting is `Don't show diffs`, diffs + will not be shown. + + Output with the "added and removed" option looks like this: + + .. + + .. image:: ../_static/diffs-show-proof.png + :alt: coqide with Set Diffs on with compacted hypotheses + Controlling the effect of proof editing commands ------------------------------------------------ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5148fa84c9..d6db305300 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -57,15 +57,14 @@ to represent :g:`(and A B)`: Notations must be in double quotes, except when the abbreviation has the form of an ordinary applicative expression; see :ref:`Abbreviations`. The notation consists of *tokens* separated by -spaces. Alphanumeric strings (such as ``A`` and ``B``) are the *parameters* +spaces. Tokens which are identifiers (such as ``A``, ``x0'``, etc.) are the *parameters* of the notation. Each of them must occur at least once in the abbreviated term. The other elements of the string (such as ``/\``) are the *symbols*. -Substrings enclosed in single quotes are treated as literals. This is necessary -for substrings that would otherwise be interpreted as :n:`@ident`\s. Similarly, -every symbol of at least 3 characters and starting with a simple quote -must be quoted (then it starts by two single quotes). Here is an -example. +Identifiers enclosed in single quotes are treated as symbols and thus +lose their role of parameters. In the same vein, every symbol of at +least 3 characters and starting with a simple quote must be quoted +(then it starts with two single quotes). Here is an example. .. coqtop:: in @@ -82,7 +81,8 @@ associativity rules have to be given. The right-hand side of a notation is interpreted at the time the notation is given. In particular, disambiguation of constants, :ref:`implicit arguments <ImplicitArguments>` and other notations are resolved at the - time of the declaration of the notation. + time of the declaration of the notation. The right-hand side is + currently typed only at use time but this may change in the future. Precedences and associativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -299,12 +299,29 @@ Notations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. -.. note:: Sometimes, a notation is expected only for the parser. To do - so, the option ``only parsing`` is allowed in the list of :n:`@syntax_modifier`\s - in :cmd:`Notation`. Conversely, the ``only printing`` :n:`@syntax_modifier` can be - used to declare that a notation should only be used for printing and - should not declare a parsing rule. In particular, such notations do - not modify the parser. +.. note:: + + The default for a notation is to be used both for parsing and + printing. It is possible to declare a notation only for parsing by + adding the option ``only parsing`` to the list of + :n:`@syntax_modifier`\s of :cmd:`Notation`. Symmetrically, the + ``only printing`` :n:`@syntax_modifier` can be used to declare that + a notation should only be used for printing. + + If a notation to be used both for parsing and printing is + overriden, both the parsing and printing are invalided, even if the + overriding rule is only parsing. + + If a given notation string occurs only in ``only printing`` rules, + the parser is not modified at all. + + To a given notation string and scope can be attached at most one + notation with both parsing and printing or with only + parsing. Contrastingly, an arbitrary number of ``only printing`` + notations differing in their right-hand sides but only a unique + right-hand side can be attached to a given string and + scope. Obviously, expressions printed by means of such extra + printing rules will not be reparsed to the same form. The Infix command ~~~~~~~~~~~~~~~~~~ |
