diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/changes.rst | 3 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 9 |
5 files changed, 10 insertions, 17 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 726a6309d4..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:** 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..d8c4fb61c2 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:: diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index b7f2927000..3649202b45 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -522,7 +522,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 73f90b0056..f454f4313d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -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>`. |