diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/changes.rst | 22 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/index.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 11 |
6 files changed, 48 insertions, 35 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 8fb03879e8..fcb150e3da 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -370,7 +370,8 @@ Notations by Pierre Roux, review by Jason Gross and Jim Fehrle for the reference manual). - **Added:** - Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` + Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t`. + This feature is considered experimental. (`#12765 <https://github.com/coq/coq/pull/12765>`_, by Hugo Herbelin). - **Added:** @@ -2017,6 +2018,25 @@ Changes in 8.12.1 fixes `#12332 <https://github.com/coq/coq/issues/12332>`_, by Théo Zimmermann and Jim Fehrle). +Changes in 8.12.2 +~~~~~~~~~~~~~~~~~ + +**Notations** + +- **Fixed:** + 8.12 regression causing notations mentioning a coercion to be ignored + (`#13436 <https://github.com/coq/coq/pull/13436>`_, + fixes `#13432 <https://github.com/coq/coq/issues/13432>`_, + by Hugo Herbelin). + +**Tactics** + +- **Fixed:** + 8.12 regression: incomplete inference of implicit arguments in :tacn:`exists` + (`#13468 <https://github.com/coq/coq/pull/13468>`_, + fixes `#13456 <https://github.com/coq/coq/issues/13456>`_, + by Hugo Herbelin). + Version 8.11 ------------ diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 246568d3c1..bce88cebde 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -220,7 +220,7 @@ html_context = { ("dev", "https://coq.github.io/doc/master/refman/"), ("stable", "https://coq.inria.fr/distrib/current/refman/"), ("v8.13", "https://coq.github.io/doc/v8.13/refman/"), - ("8.12", "https://coq.inria.fr/distrib/V8.12.1/refman/"), + ("8.12", "https://coq.inria.fr/distrib/V8.12.2/refman/"), ("8.11", "https://coq.inria.fr/distrib/V8.11.2/refman/"), ("8.10", "https://coq.inria.fr/distrib/V8.10.2/refman/"), ("8.9", "https://coq.inria.fr/distrib/V8.9.1/refman/"), diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8f5c045929..b2ebd96607 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -264,17 +264,6 @@ These patterns can be used when the hypothesis is an equality: :n:`@simple_intropattern_closed`. :ref:`Example <intropattern_injection_ex>` -.. flag:: Bracketing Last Introduction Pattern - - For :n:`intros @intropattern_list`, controls how to handle a - conjunctive pattern that doesn't give enough simple patterns to match - all the arguments in the constructor. If set (the default), Coq generates - additional names to match the number of arguments. - Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more - similar to |SSR|'s intro patterns. - - .. deprecated:: 8.10 - .. _intropattern_cons_note: .. note:: @@ -1641,17 +1630,21 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. .. tacv:: instantiate (@natural := @term) - This variant allows to refer to an existential variable which was not named - by the user. The :n:`@natural` argument is the position of the existential variable - from right to left in the goal. Because this variant is not robust to slight - changes in the goal, its use is strongly discouraged. + This variant selects an existential variable by its position. The + :n:`@natural` argument is the position of the existential variable + *from right to left* in the conclusion of the goal. (Use one of + the variants below to select an existential variable in a + hypothesis.) Counting starts at 1 and multiple occurrences of the + same existential variable are counted multiple times. Because this + variant is not robust to slight changes in the goal, its use is + strongly discouraged. .. tacv:: instantiate ( @natural := @term ) in @ident instantiate ( @natural := @term ) in ( value of @ident ) instantiate ( @natural := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a - hypothesis or in the body or the type of a local definition. + hypothesis or in the body or the type of a local definition (named :n:`@ident`). .. tacv:: instantiate diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst index 7724d7433c..63ddbd0a3a 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -10,19 +10,16 @@ the user and the assistant. The building blocks for this dialog are tactics which the user will use to represent steps in the proof of a theorem. -Incomplete proofs have one or more open (unproven) sub-goals. Each -goal has its own context (a set of assumptions that can be used to -prove the goal). Tactics can transform goals and contexts. -Internally, the incomplete proof is represented as a partial proof -term, with holes for the unproven sub-goals. +The first section presents the proof mode (the core mechanism of the +dialog between the user and the proof assistant). Then, several +sections describe the available tactics. One section covers the +SSReflect proof language, which provides a consistent alternative set +of tactics to the standard basic tactics. The last section documents +the ``Scheme`` family of commands, which can be used to extend the +power of the :tacn:`induction` and :tacn:`inversion` tactics. -When a proof is complete, the user leaves the proof mode and defers -the verification of the resulting proof term to the :ref:`kernel -<core-language>`. - -This chapter is divided in several parts, describing the basic ideas -of the proof mode (during which tactics can be used), and several -flavors of tactics, including the SSReflect proof language. +Additional tactics are documented in the next chapter +:ref:`automatic-tactics`. .. toctree:: :maxdepth: 1 diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index d271145af8..90404b7321 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -525,7 +525,7 @@ the conversion in hypotheses :n:`{+ @ident}`. use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls. - The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + The :tacn:`cbn` tactic was intended to be a more principled, faster and more predictable replacement for :tacn:`simpl`. The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 4dbf3b150b..f454f4313d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -309,7 +309,7 @@ at the time of use of the notation. 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 + overridden, 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, @@ -857,7 +857,8 @@ example showing a notation for a chain of equalities. It relies on an artificial expansion of the intended denotation so as to expose a ``φ(x, .. φ(y,t) ..)`` structure, with the drawback that if ever the beta-redexes are contracted, the notations stops to be used for -printing. +printing. Support for notations defined in this way should be considered +experimental. .. coqtop:: in @@ -1740,7 +1741,8 @@ Number notations Note that only fully-reduced ground terms (terms containing only function application, constructors, inductive type families, - sorts, and primitive integers) will be considered for printing. + sorts, primitive integers, primitive floats, primitive arrays and type + constants for primitive types) will be considered for printing. .. _number-string-via: @@ -1904,7 +1906,8 @@ String notations Note that only fully-reduced ground terms (terms containing only function application, constructors, inductive type families, - sorts, and primitive integers) will be considered for printing. + sorts, primitive integers, primitive floats, primitive arrays and type + constants for primitive types) will be considered for printing. :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` works as for :ref:`number notations above <number-string-via>`. |