diff options
Diffstat (limited to 'doc')
23 files changed, 205 insertions, 0 deletions
diff --git a/doc/changelog/00-title.rst b/doc/changelog/00-title.rst new file mode 100644 index 0000000000..628d9c8578 --- /dev/null +++ b/doc/changelog/00-title.rst @@ -0,0 +1,2 @@ +Unreleased changes +------------------ diff --git a/doc/changelog/01-kernel/00000-title.rst b/doc/changelog/01-kernel/00000-title.rst new file mode 100644 index 0000000000..f680628a05 --- /dev/null +++ b/doc/changelog/01-kernel/00000-title.rst @@ -0,0 +1,3 @@ + +**Kernel** + diff --git a/doc/changelog/02-specification-language/00000-title.rst b/doc/changelog/02-specification-language/00000-title.rst new file mode 100644 index 0000000000..99bd2c5b44 --- /dev/null +++ b/doc/changelog/02-specification-language/00000-title.rst @@ -0,0 +1,3 @@ + +**Specification language, type inference** + diff --git a/doc/changelog/03-notations/00000-title.rst b/doc/changelog/03-notations/00000-title.rst new file mode 100644 index 0000000000..abc532df11 --- /dev/null +++ b/doc/changelog/03-notations/00000-title.rst @@ -0,0 +1,3 @@ + +**Notations** + diff --git a/doc/changelog/04-tactics/00000-title.rst b/doc/changelog/04-tactics/00000-title.rst new file mode 100644 index 0000000000..3c7802d632 --- /dev/null +++ b/doc/changelog/04-tactics/00000-title.rst @@ -0,0 +1,3 @@ + +**Tactics** + diff --git a/doc/changelog/04-tactics/09996-hint-mode.rst b/doc/changelog/04-tactics/09996-hint-mode.rst new file mode 100644 index 0000000000..06e9059b45 --- /dev/null +++ b/doc/changelog/04-tactics/09996-hint-mode.rst @@ -0,0 +1,5 @@ +- Modes are now taken into account by :tacn:`typeclasses eauto` for + local hypotheses + (`#9996 <https://github.com/coq/coq/pull/9996>`_, + fixes `#5752 <https://github.com/coq/coq/issues/5752>`_, + by Maxime Dénès, review by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/10059-change-no-check.rst b/doc/changelog/04-tactics/10059-change-no-check.rst new file mode 100644 index 0000000000..987b2a8ccd --- /dev/null +++ b/doc/changelog/04-tactics/10059-change-no-check.rst @@ -0,0 +1,7 @@ +- New variant :tacn:`change_no_check` of :tacn:`change`, usable as a + documented replacement of :tacn:`convert_concl_no_check` + (`#10012 <https://github.com/coq/coq/pull/10012>`_, + `#10017 <https://github.com/coq/coq/pull/10017>`_, + `#10053 <https://github.com/coq/coq/pull/10053>`_, and + `#10059 <https://github.com/coq/coq/pull/10059>`_, + by Hugo Herbelin and Paolo G. Giarrusso). diff --git a/doc/changelog/05-tactic-language/00000-title.rst b/doc/changelog/05-tactic-language/00000-title.rst new file mode 100644 index 0000000000..b34d190298 --- /dev/null +++ b/doc/changelog/05-tactic-language/00000-title.rst @@ -0,0 +1,3 @@ + +**Tactic language** + diff --git a/doc/changelog/06-ssreflect/00000-title.rst b/doc/changelog/06-ssreflect/00000-title.rst new file mode 100644 index 0000000000..2e724627ec --- /dev/null +++ b/doc/changelog/06-ssreflect/00000-title.rst @@ -0,0 +1,3 @@ + +**SSReflect** + diff --git a/doc/changelog/06-ssreflect/09995-notations.rst b/doc/changelog/06-ssreflect/09995-notations.rst new file mode 100644 index 0000000000..3dfc45242d --- /dev/null +++ b/doc/changelog/06-ssreflect/09995-notations.rst @@ -0,0 +1,8 @@ +- `inE` now expands `y \in r x` when `r` is a `simpl_rel`. + New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion + class, simplified `predType` interface: `pred_class` and `mkPredType` + deprecated, `{pred T}` and `PredType` should be used instead. + `if c return t then ...` now expects `c` to be a variable bound in `t`. + New `nonPropType` interface matching types that do _not_ have sort `Prop`. + New `relpre R f` definition for the preimage of a relation R under f + (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). diff --git a/doc/changelog/07-commands-and-options/00000-title.rst b/doc/changelog/07-commands-and-options/00000-title.rst new file mode 100644 index 0000000000..1a0272983e --- /dev/null +++ b/doc/changelog/07-commands-and-options/00000-title.rst @@ -0,0 +1,3 @@ + +**Commands and options** + diff --git a/doc/changelog/08-tools/00000-title.rst b/doc/changelog/08-tools/00000-title.rst new file mode 100644 index 0000000000..bf462744fb --- /dev/null +++ b/doc/changelog/08-tools/00000-title.rst @@ -0,0 +1,3 @@ + +**Tools** + diff --git a/doc/changelog/09-coqide/00000-title.rst b/doc/changelog/09-coqide/00000-title.rst new file mode 100644 index 0000000000..0fc27cf380 --- /dev/null +++ b/doc/changelog/09-coqide/00000-title.rst @@ -0,0 +1,3 @@ + +**CoqIDE** + diff --git a/doc/changelog/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst new file mode 100644 index 0000000000..d517a0e709 --- /dev/null +++ b/doc/changelog/10-standard-library/00000-title.rst @@ -0,0 +1,3 @@ + +**Standard library** + diff --git a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst new file mode 100644 index 0000000000..732c088f45 --- /dev/null +++ b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst @@ -0,0 +1,3 @@ +- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` + (`#9984 <https://github.com/coq/coq/pull/9984>`_, + by Jean-Christophe Léchenet and Oliver Nash). diff --git a/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst new file mode 100644 index 0000000000..6b301f59d3 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst @@ -0,0 +1,3 @@ + +**Infrastructure and dependencies** + diff --git a/doc/changelog/12-misc/00000-title.rst b/doc/changelog/12-misc/00000-title.rst new file mode 100644 index 0000000000..5e709e2b27 --- /dev/null +++ b/doc/changelog/12-misc/00000-title.rst @@ -0,0 +1,3 @@ + +**Miscellaneous** + diff --git a/doc/changelog/12-misc/09964-changes.rst b/doc/changelog/12-misc/09964-changes.rst new file mode 100644 index 0000000000..1113782180 --- /dev/null +++ b/doc/changelog/12-misc/09964-changes.rst @@ -0,0 +1,13 @@ +- Changelog has been moved from a specific file `CHANGES.md` to the + reference manual; former Credits chapter of the reference manual has + been split in two parts: a History chapter which was enriched with + additional historical information about Coq versions 1 to 5, and a + Changes chapter which was enriched with the content formerly in + `CHANGES.md` and `COMPATIBILITY` + (`#9133 <https://github.com/coq/coq/pull/9133>`_, + `#9668 <https://github.com/coq/coq/pull/9668>`_, + `#9939 <https://github.com/coq/coq/pull/9939>`_, + `#9964 <https://github.com/coq/coq/pull/9964>`_, + by Théo Zimmermann, + with help and ideas from Emilio Jesús Gallego Arias, + Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). diff --git a/doc/changelog/README.md b/doc/changelog/README.md new file mode 100644 index 0000000000..2891eb207e --- /dev/null +++ b/doc/changelog/README.md @@ -0,0 +1,41 @@ +# Unreleased changelog # + +## When to add an entry? ## + +All new features, user-visible changes to features, user-visible or +otherwise important infrastructure changes, and important bug fixes +should get a changelog entry. + +Compatibility-breaking changes should always get a changelog entry, +which should explain what compatibility-breakage is to expect. + +Pull requests changing the ML API in significant ways should add an +entry in [`dev/doc/changes.md`](../../dev/doc/changes.md). + +## How to add an entry? ## + +You should create a file in one of the sub-directories. The name of +the file should be `NNNNN-identifier.rst` where `NNNNN` is the number +of the pull request on five digits and `identifier` is whatever you +want. + +This file should use the same format as the reference manual (as it +will be copied in there). You may reference the documentation you just +added with `:ref:`, `:tacn:`, `:cmd:`, `:opt:`, `:token:`, etc. See +the [documentation of the Sphinx format](../sphinx/README.rst) of the +manual for details. + +The entry should be written using the following structure: + +``` rst +- Description of the changes, with possible link to + :ref:`relevant-section` of the updated documentation + (`#PRNUM <https://github.com/coq/coq/pull/PRNUM>`_, + [fixes `#ISSUE1 <https://github.com/coq/coq/issues/ISSUE1>`_ + [ and `#ISSUE2 <https://github.com/coq/coq/issues/ISSUE2>`_],] + by Full Name[, with help / review of Full Name]). +``` + +The description should be kept rather short and the only additional +required meta-information are the link to the pull request and the +full name of the author. @@ -11,6 +11,7 @@ (package coq) (source_tree sphinx) (source_tree tools) + unreleased.rst (env_var SPHINXWARNOPT)) (action (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) @@ -19,6 +20,11 @@ (name refman-html) (deps sphinx_build)) +(rule + (targets unreleased.rst) + (deps (source_tree changelog)) + (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst")))) + ; The install target still needs more work. ; (install ; (section doc) diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index a5e9023732..77a6ee79cc 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -405,6 +405,8 @@ few other commands related to typeclasses. resolution with the local hypotheses use full conversion during unification. + + When considering local hypotheses, we use the union of all the modes + declared in the given databases. .. cmdv:: typeclasses eauto @num diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 1c4c748295..5704587ae0 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -2,6 +2,8 @@ Recent changes -------------- +.. include:: ../unreleased.rst + Version 8.10 ------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8d9e99b9d5..1f339e7761 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4811,3 +4811,83 @@ references to automatically generated names. :name: Mangle Names Prefix Specifies the prefix to use when generating names. + +Performance-oriented tactic variants +------------------------------------ + +.. tacn:: change_no_check @term + :name: change_no_check + + For advanced usage. Similar to :n:`change @term`, but as an optimization, + it skips checking that :n:`@term` is convertible to the goal. + + Recall that the Coq kernel typechecks proofs again when they are concluded to + ensure safety. Hence, using :tacn:`change` checks convertibility twice + overall, while :tacn:`change_no_check` can produce ill-typed terms, + but checks convertibility only once. + Hence, :tacn:`change_no_check` can be useful to speed up certain proof + scripts, especially if one knows by construction that the argument is + indeed convertible to the goal. + + In the following example, :tacn:`change_no_check` replaces :g:`False` by + :g:`True`, but :g:`Qed` then rejects the proof, ensuring consistency. + + .. example:: + + .. coqtop:: all abort + + Goal False. + change_no_check True. + exact I. + Fail Qed. + + .. tacv:: convert_concl_no_check @term + :name: convert_concl_no_check + + Deprecated old name for :tacn:`change_no_check`. Does not support any of its + variants. + +.. tacn:: exact_no_check @term + :name: exact_no_check + + For advanced usage. Similar to :n:`exact @term`, but as an optimization, + it skips checking that :n:`@term` has the goal's type, relying on the kernel + check instead. See :tacn:`change_no_check` for more explanations. + + .. example:: + + .. coqtop:: all abort + + Goal False. + exact_no_check I. + Fail Qed. + + .. tacv:: vm_cast_no_check @term + :name: vm_cast_no_check + + For advanced usage. Similar to :n:`exact_no_check @term`, but additionally + instructs the kernel to use :tacn:`vm_compute` to compare the + goal's type with the :n:`@term`'s type. + + .. example:: + + .. coqtop:: all abort + + Goal False. + vm_cast_no_check I. + Fail Qed. + + .. tacv:: native_cast_no_check @term + :name: native_cast_no_check + + for advanced usage. similar to :n:`exact_no_check @term`, but additionally + instructs the kernel to use :tacn:`native_compute` to compare the goal's + type with the :n:`@term`'s type. + + .. example:: + + .. coqtop:: all abort + + Goal False. + native_cast_no_check I. + Fail Qed. |