diff options
Diffstat (limited to 'doc')
10 files changed, 70 insertions, 20 deletions
diff --git a/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst b/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst deleted file mode 100644 index 6cab6a1c13..0000000000 --- a/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Fix proof of False when using |SProp| (incorrect De Bruijn handling - when inferring the relevance mark of a function) (`#10904 - <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot). diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst new file mode 100644 index 0000000000..327a39bdb6 --- /dev/null +++ b/doc/changelog/03-notations/10963-simplify-parser.rst @@ -0,0 +1,6 @@ +- A simplification of parsing rules could cause a slight change of + parsing precedences for the very rare users who defined notations + with `constr` at level strictly between 100 and 200 and used these + notations on the right-hand side of a cast operator (`:`, `:>`, + `:>>`) (`#10963 <https://github.com/coq/coq/pull/10963>`_, by Théo + Zimmermann, simplification initially noticed by Jim Fehrle). diff --git a/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst b/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst deleted file mode 100644 index 9d15b7126f..0000000000 --- a/doc/changelog/05-tactic-language/10899-master+fix10894-regression-ltac-uconstr-typing.rst +++ /dev/null @@ -1 +0,0 @@ -- Fixed bug #10894: Ltac1 regression in binding free names in uconstr (`#10899 <https://github.com/coq/coq/pull/10899>`_, by Hugo Herbelin). diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst new file mode 100644 index 0000000000..5d8467025b --- /dev/null +++ b/doc/changelog/10-standard-library/10827-dedekind-reals.rst @@ -0,0 +1,11 @@ +- New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers + as boolean-values functions along with 3 logical axioms: limited principle + of omniscience, excluded middle of negations and functional extensionality. + The exposed type :g:`R` in module :g:`Reals.Rdefinitions` is those + Dedekind reals, hidden behind an opaque module. + Classical Dedekind reals are a quotient of constructive reals, which allows + to transport many constructive proofs to the classical case. + + See `#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria, + based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin, + code review by Hugo Herbelin. diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 9dd4700db5..307214089f 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -9,4 +9,4 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.Definition ~opaque:false sigma udecl body None [] + ~kind:Decls.(IsDefinition Definition) ~opaque:false sigma udecl body None [] diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index b6fcf9da22..80a24b997c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -726,6 +726,45 @@ Changes in 8.10.0 fixes `#9512 <https://github.com/coq/coq/issues/9512>`_ by Vincent Laporte). +Changes in 8.10.1 +~~~~~~~~~~~~~~~~~ + +A few bug fixes and documentation improvements, in particular: + +**Kernel** + +- Fix proof of False when using |SProp| (incorrect De Bruijn handling + when inferring the relevance mark of a function) (`#10904 + <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot). + +**Tactics** + +- Fix an anomaly when unsolved evar in :cmd:`Add Ring` + (`#10891 <https://github.com/coq/coq/pull/10891>`_, + fixes `#9851 <https://github.com/coq/coq/issues/9851>`_, + by Gaëtan Gilbert). + +**Tactic language** + +- Fix Ltac regression in binding free names in uconstr + (`#10899 <https://github.com/coq/coq/pull/10899>`_, + fixes `#10894 <https://github.com/coq/coq/issues/10894>`_, + by Hugo Herbelin). + +**CoqIDE** + +- Fix handling of unicode input before space + (`#10852 <https://github.com/coq/coq/pull/10852>`_, + fixes `#10842 <https://github.com/coq/coq/issues/10842>`_, + by Arthur Charguéraud). + +**Extraction** + +- Fix custom extraction of inductives to JSON + (`#10897 <https://github.com/coq/coq/pull/10897>`_, + fixes `#4741 <https://github.com/coq/coq/issues/4741>`_, + by Helge Bahmann). + Version 8.9 ----------- diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 03b30d5d97..57a54bc0ad 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -538,13 +538,11 @@ Requesting information .. cmdv:: Show Proof :name: Show Proof - It displays the proof term generated by the tactics - that have been applied. If the proof is not completed, this term - contain holes, which correspond to the sub-terms which are still to be - constructed. These holes appear as a question mark indexed by an - integer, and applied to the list of variables in the context, since it - may depend on them. The types obtained by abstracting away the context - from the type of each placeholder are also printed. + Displays the proof term generated by the tactics + that have been applied so far. If the proof is incomplete, the term + will contain holes, which correspond to subterms which are still to be + constructed. Each hole is an existential variable, which appears as a + question mark followed by an identifier. .. cmdv:: Show Conjectures :name: Show Conjectures @@ -574,9 +572,8 @@ Requesting information .. cmdv:: Show Existentials :name: Show Existentials - It displays the set of all uninstantiated - existential variables in the current proof tree, along with the type - and the context of each variable. + Displays all open goals / existential variables in the current proof + along with the type and the context of each variable. .. cmdv:: Show Match @ident diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1d08001e34..75897fec45 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2670,7 +2670,7 @@ context entry name. Lemma test n m (H : m + 1 < n) : True. have @i : 'I_n by apply: (Sub m); omega. -Note that the sub-term produced by :tacn:`omega` is in general huge and +Note that the subterm produced by :tacn:`omega` is in general huge and uninteresting, and hence one may want to hide it. For this purpose the ``[: name ]`` intro pattern and the tactic ``abstract`` (see :ref:`abstract_ssr`) are provided. @@ -4583,7 +4583,7 @@ The ``elim/`` tactic distinguishes two cases: passed to the eliminator as the last argument (``x`` in ``foo_ind``) and ``en−1 … e1`` are used as patterns to select in the goal the occurrences that will be bound by the predicate ``P``, thus it must be possible to unify - the sub-term of the goal matched by ``en−1`` with ``pm`` , the one matched + the subterm of the goal matched by ``en−1`` with ``pm`` , the one matched by ``en−2`` with ``pm−1`` and so on. :regular eliminator: in all the other cases. Here it must be possible to unify the term matched by ``en`` with ``pm`` , the one matched by diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index bcc5e914ac..a28ce600ca 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -750,12 +750,12 @@ level is otherwise given explicitly by using the syntax Levels are cumulative: a notation at level ``n`` of which the left end is a term shall use rules at level less than ``n`` to parse this -sub-term. More precisely, it shall use rules at level strictly less +subterm. More precisely, it shall use rules at level strictly less than ``n`` if the rule is declared with ``right associativity`` and rules at level less or equal than ``n`` if the rule is declared with ``left associativity``. Similarly, a notation at level ``n`` of which the right end is a term shall use by default rules at level strictly -less than ``n`` to parse this sub-term if the rule is declared left +less than ``n`` to parse this subterm if the rule is declared left associative and rules at level less or equal than ``n`` if the rule is declared right associative. This is what happens for instance in the rule diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 75c8c6c1ea..f0ada745e7 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -68,6 +68,7 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/WKL.v theories/Logic/FinFun.v theories/Logic/PropFacts.v + theories/Logic/HLevels.v </dd> <dt> <b>Structures</b>: @@ -518,8 +519,8 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/ConstructiveRealsMorphisms.v theories/Reals/ConstructiveCauchyReals.v theories/Reals/ConstructiveCauchyRealsMult.v + theories/Reals/ClassicalDedekindReals.v theories/Reals/Raxioms.v - theories/Reals/ConstructiveRIneq.v theories/Reals/ConstructiveRealsLUB.v theories/Reals/RIneq.v theories/Reals/DiscrR.v |