diff options
Diffstat (limited to 'doc')
12 files changed, 44 insertions, 25 deletions
diff --git a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst new file mode 100644 index 0000000000..32526babdb --- /dev/null +++ b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst @@ -0,0 +1,8 @@ +- **Added:** + :cmd:`Arguments <Arguments (implicits)>` now supports setting + implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`. + (`#11098 <https://github.com/coq/coq/pull/11098>`_, + by Hugo Herbelin, fixes `#4696 + <https://github.com/coq/coq/pull/4696>`_, `#5173 + <https://github.com/coq/coq/pull/5173>`_, `#9098 + <https://github.com/coq/coq/pull/9098>`_.). diff --git a/doc/changelog/03-notations/11113-remove-compat.rst b/doc/changelog/03-notations/11113-remove-compat.rst index 8c71d70cda..3bcdd3dd6f 100644 --- a/doc/changelog/03-notations/11113-remove-compat.rst +++ b/doc/changelog/03-notations/11113-remove-compat.rst @@ -1,4 +1,4 @@ -- Removed deprecated ``compat`` modifier of :cmd:`Notation` +- **Removed:** deprecated ``compat`` modifier of :cmd:`Notation` and :cmd:`Infix` commands (`#11113 <https://github.com/coq/coq/pull/11113>`_, by Théo Zimmermann, with help from Jason Gross). diff --git a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst index 8551cf3aac..f377b53ae2 100644 --- a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst +++ b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst @@ -1,2 +1,3 @@ -- The printing algorithm now interleave search for notations and removal of coercions +- **Changed:** + The printing algorithm now interleaves search for notations and removal of coercions (`#11172 <https://github.com/coq/coq/pull/11172>`_, by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst index 2815f8af8a..eeae2ec519 100644 --- a/doc/changelog/04-tactics/10760-more-rapply.rst +++ b/doc/changelog/04-tactics/10760-more-rapply.rst @@ -1,4 +1,5 @@ -- The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles +- **Changed:** + The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles arbitrary numbers of underscores and takes in a :g:`uconstr`. In rare cases where users were relying on :tacn:`rapply` inserting exactly 15 underscores and no more, due to the lemma having a diff --git a/doc/changelog/07-commands-and-options/11162-local-cs.rst b/doc/changelog/07-commands-and-options/11162-local-cs.rst index 5a69a107cd..638222fbe1 100644 --- a/doc/changelog/07-commands-and-options/11162-local-cs.rst +++ b/doc/changelog/07-commands-and-options/11162-local-cs.rst @@ -1 +1,3 @@ -- Handle the ``#[local]`` attribute in :g:`Canonical Structure` declarations (`#11162 <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). +- **Added:** Handle the ``#[local]`` attribute in :g:`Canonical + Structure` declarations (`#11162 + <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst index b9ecd140e7..ec34c075ae 100644 --- a/doc/changelog/07-commands-and-options/11164-let-cs.rst +++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst @@ -1 +1,3 @@ -- A section variable introduces with :g:`Let` can be declared as a :g:`Canonical Structure` (`#11164 <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). +- **Added:** A section variable introduces with :g:`Let` can be + declared as a :g:`Canonical Structure` (`#11164 + <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index b0197c500c..f706633da9 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,6 +35,11 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. opt:: Dump Arith + + This option (unset by default) may be set to a file path where + debug info will be written. + .. cmd:: Show Lia Profile This command prints some statistics about the amount of pivoting diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 7b4b652a6a..f0bbaed8f3 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1583,7 +1583,7 @@ An implicit argument is considered trailing when all following arguments are dec implicit. Trailing implicit arguments cannot be declared non maximally inserted, otherwise they would never be inserted. -.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. +.. exn:: Argument @name is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. For instance: @@ -1713,11 +1713,11 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmd:: Arguments @qualid {* {| [ @name ] | { @name } | @name } } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, - where the list of possibly bracketed :token:`ident` is a prefix of the list of + where the list of possibly bracketed :token:`name` is a prefix of the list of arguments of :token:`qualid` where the ones to be declared implicit are surrounded by square brackets and the ones to be declared as maximally inserted implicits are surrounded by curly braces. @@ -1731,20 +1731,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmdv:: Global Arguments @qualid {* {| [ @name ] | { @name } | @name } } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmdv:: Local Arguments @qualid {* {| [ @name ] | { @name } | @name } } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } } +.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @name ] | { @name } | @name } } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 09090ce89a..721c7a7a51 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1063,6 +1063,9 @@ Parameterized inductive types | cons3 : A -> list3 -> list3. End list3. + Attributes ``uniform`` and ``nonuniform`` respectively enable and + disable uniform parameters for a single inductive declaration block. + .. seealso:: Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e5edd08995..3d1fc6d4b9 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -545,7 +545,7 @@ Computing Module dependencies In order to compute module dependencies (to be used by ``make`` or ``dune``), |Coq| provides the ``coqdep`` tool. -``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +``coqdep`` computes inter-module dependencies for |Coq| programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at. @@ -554,11 +554,6 @@ Dependencies of |Coq| modules are computed by looking at ``Require`` commands (``Require``, ``Require Export``, ``Require Import``), but also at the command ``Declare ML Module``. -Dependencies of |OCaml| modules are computed by looking at -`open` commands and the dot notation *module.value*. However, this is -done approximately and you are advised to use ``ocamldep`` instead for the -|OCaml| module dependencies. - See the man page of ``coqdep`` for more details and options. Both Dune and ``coq_makefile`` use ``coqdep`` to compute the diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 1f9178f4b6..85d86bed62 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -270,7 +270,7 @@ class GallinaObject(PlainObject): :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. """ subdomain = "thm" - index_suffix = "(thm)" + index_suffix = "(theorem)" annotation = "Theorem" class VernacObject(NotationObject): @@ -283,7 +283,7 @@ class VernacObject(NotationObject): This command is equivalent to :n:`…`. """ subdomain = "cmd" - index_suffix = "(cmd)" + index_suffix = "(command)" annotation = "Command" def _name_from_signature(self, signature): @@ -306,7 +306,7 @@ class VernacVariantObject(VernacObject): This is equivalent to :n:`Axiom @ident : @term`. """ - index_suffix = "(cmdv)" + index_suffix = "(command variant)" annotation = "Variant" def _name_from_signature(self, signature): @@ -322,7 +322,7 @@ class TacticNotationObject(NotationObject): :token:`expr` is evaluated to ``v`` which must be a tactic value. … """ subdomain = "tacn" - index_suffix = "(tacn)" + index_suffix = "(tactic)" annotation = None class TacticNotationVariantObject(TacticNotationObject): @@ -342,7 +342,7 @@ class TacticNotationVariantObject(TacticNotationObject): The number is the failure level. If no level is specified, it defaults to 0. … """ - index_suffix = "(tacnv)" + index_suffix = "(tactic variant)" annotation = "Variant" class OptionObject(NotationObject): @@ -357,7 +357,7 @@ class OptionObject(NotationObject): application of a tactic. """ subdomain = "opt" - index_suffix = "(opt)" + index_suffix = "(option)" annotation = "Option" def _name_from_signature(self, signature): @@ -534,7 +534,7 @@ class ExceptionObject(NotationObject): Raised if :n:`@tactic` does not fully solve the goal. """ subdomain = "exn" - index_suffix = "(err)" + index_suffix = "(error)" annotation = "Error" # Uses “exn” since “err” already is a CSS class added by “writer_aux”. @@ -557,7 +557,7 @@ class WarningObject(NotationObject): valid coercion paths are ignored. """ subdomain = "warn" - index_suffix = "(warn)" + index_suffix = "(warning)" annotation = "Warning" # Generate names automatically diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index ab18d136b8..5659a64b84 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -80,9 +80,11 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): while atom != "": if atom[0] == "'": node += nodes.raw("\\textquotesingle{}", "\\textquotesingle{}", format="latex") + node += nodes.raw("'", "'", format="html") atom = atom[1:] elif atom[0] == "`": node += nodes.raw("\\`{}", "\\`{}", format="latex") + node += nodes.raw("`", "`", format="html") atom = atom[1:] else: index_ap = atom.find("'") |