From dd0019e5a02db64012d2c3f6692ad03c3a84924f Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 2 Nov 2019 18:08:28 +0100 Subject: Move unreleased changelog to new 8.11 section. --- doc/changelog/01-kernel/09867-floats.rst | 14 - .../10439-uniform-opaque-seff-handling.rst | 5 - .../01-kernel/10664-sections-stack-in-kernel.rst | 7 - doc/changelog/01-kernel/10811-sprop-default-on.rst | 4 - .../02-specification-language/10049-bidi-app.rst | 7 - .../10076-not-canonical-projection.rst | 5 - .../10167-orpat-mixfix.rst | 15 - .../10215-rm-maybe-open-proof.rst | 13 - .../10441-static-poly-section.rst | 13 - .../02-specification-language/10758-fix-10757.rst | 6 - .../10985-about-arguments.rst | 6 - .../10996-refine-instance-returns.rst | 4 - .../10997-unsupport-atts-warn.rst | 4 - ...32-master+fix-implicit-let-fixpoint-bug3282.rst | 13 - .../03-notations/09883-numeral-notations-sorts.rst | 5 - .../03-notations/10180-deprecate-notations.rst | 11 - .../03-notations/10963-simplify-parser.rst | 7 - doc/changelog/04-tactics/09288-injection-as.rst | 5 - doc/changelog/04-tactics/09856-zify.rst | 8 - .../04-tactics/10318-select-only-error.rst | 5 - .../04-tactics/10765-micromega-caches.rst | 4 - doc/changelog/04-tactics/10774-zify-Z_to_N.rst | 4 - .../04-tactics/10966-assert-succeeds-once.rst | 13 - doc/changelog/05-tactic-language/10002-ltac2.rst | 10 - .../10289-ltac2+delimited-constr-in-notations.rst | 6 - .../10324-ltac2-ssr-ampersand.rst | 6 - .../06-ssreflect/10022-ssr-under-setoid.rst | 29 -- doc/changelog/06-ssreflect/10932-void-type-ssr.rst | 4 - doc/changelog/06-ssreflect/11136-inj_compr.rst | 2 - .../07-commands-and-options/09530-rm-unknown.rst | 7 - .../10185-instance-no-bang.rst | 3 - .../10277-no-show-script.rst | 3 - .../07-commands-and-options/10291-typing-flags.rst | 5 - .../07-commands-and-options/10476-fix-export.rst | 6 - .../10489-print_dependent_evars.rst | 8 - .../10494-diffs-in-show-proof.rst | 7 - .../11187-remove-addpath.rst | 5 - doc/changelog/08-tools/08642-vos-files.rst | 8 - .../08-tools/10245-require-command-line.rst | 7 - doc/changelog/08-tools/10947-coq-makefile-dep.rst | 6 - doc/changelog/08-tools/11068-coqbin-noslash.rst | 3 - .../09772-ordered_type-hint-db.rst | 5 - .../09811-remove-zlogarithm.rst | 4 - .../10445-constructive-reals.rst | 17 - .../10651-new-lemmas-for-lists.rst | 9 - .../10-standard-library/10827-dedekind-reals.rst | 12 - ...10895-master+weak-excluded-middle-de-morgan.rst | 4 - .../10471-ocaml-408.rst | 5 - doc/sphinx/changes.rst | 395 +++++++++++++++++++++ 49 files changed, 395 insertions(+), 359 deletions(-) delete mode 100644 doc/changelog/01-kernel/09867-floats.rst delete mode 100644 doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst delete mode 100644 doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst delete mode 100644 doc/changelog/01-kernel/10811-sprop-default-on.rst delete mode 100644 doc/changelog/02-specification-language/10049-bidi-app.rst delete mode 100644 doc/changelog/02-specification-language/10076-not-canonical-projection.rst delete mode 100644 doc/changelog/02-specification-language/10167-orpat-mixfix.rst delete mode 100644 doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst delete mode 100644 doc/changelog/02-specification-language/10441-static-poly-section.rst delete mode 100644 doc/changelog/02-specification-language/10758-fix-10757.rst delete mode 100644 doc/changelog/02-specification-language/10985-about-arguments.rst delete mode 100644 doc/changelog/02-specification-language/10996-refine-instance-returns.rst delete mode 100644 doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst delete mode 100644 doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst delete mode 100644 doc/changelog/03-notations/09883-numeral-notations-sorts.rst delete mode 100644 doc/changelog/03-notations/10180-deprecate-notations.rst delete mode 100644 doc/changelog/03-notations/10963-simplify-parser.rst delete mode 100644 doc/changelog/04-tactics/09288-injection-as.rst delete mode 100644 doc/changelog/04-tactics/09856-zify.rst delete mode 100644 doc/changelog/04-tactics/10318-select-only-error.rst delete mode 100644 doc/changelog/04-tactics/10765-micromega-caches.rst delete mode 100644 doc/changelog/04-tactics/10774-zify-Z_to_N.rst delete mode 100644 doc/changelog/04-tactics/10966-assert-succeeds-once.rst delete mode 100644 doc/changelog/05-tactic-language/10002-ltac2.rst delete mode 100644 doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst delete mode 100644 doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst delete mode 100644 doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst delete mode 100644 doc/changelog/06-ssreflect/10932-void-type-ssr.rst delete mode 100644 doc/changelog/06-ssreflect/11136-inj_compr.rst delete mode 100644 doc/changelog/07-commands-and-options/09530-rm-unknown.rst delete mode 100644 doc/changelog/07-commands-and-options/10185-instance-no-bang.rst delete mode 100644 doc/changelog/07-commands-and-options/10277-no-show-script.rst delete mode 100644 doc/changelog/07-commands-and-options/10291-typing-flags.rst delete mode 100644 doc/changelog/07-commands-and-options/10476-fix-export.rst delete mode 100644 doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst delete mode 100644 doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst delete mode 100644 doc/changelog/07-commands-and-options/11187-remove-addpath.rst delete mode 100644 doc/changelog/08-tools/08642-vos-files.rst delete mode 100644 doc/changelog/08-tools/10245-require-command-line.rst delete mode 100644 doc/changelog/08-tools/10947-coq-makefile-dep.rst delete mode 100644 doc/changelog/08-tools/11068-coqbin-noslash.rst delete mode 100644 doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst delete mode 100644 doc/changelog/10-standard-library/09811-remove-zlogarithm.rst delete mode 100644 doc/changelog/10-standard-library/10445-constructive-reals.rst delete mode 100644 doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst delete mode 100644 doc/changelog/10-standard-library/10827-dedekind-reals.rst delete mode 100644 doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst (limited to 'doc') diff --git a/doc/changelog/01-kernel/09867-floats.rst b/doc/changelog/01-kernel/09867-floats.rst deleted file mode 100644 index cae4dbb335..0000000000 --- a/doc/changelog/01-kernel/09867-floats.rst +++ /dev/null @@ -1,14 +0,0 @@ -- **Added:** - A built-in support of floating-point arithmetic, allowing - one to devise efficient reflection tactics involving numerical - computation. Primitive floats are added in the language of terms, - following the binary64 format of the IEEE 754 standard, and the - related operations are implemented for the different reduction - engines of Coq by using the corresponding processor operators in - rounding-to-nearest-even. The properties of these operators are - axiomatized in the theory :g:`Coq.Floats.FloatAxioms` which is part - of the library :g:`Coq.Floats.Floats`. - See Section :ref:`primitive-floats` - (`#9867 `_, - closes `#8276 `_, - by Guillaume Bertholon, Erik Martin-Dorel, Pierre Roux). diff --git a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst deleted file mode 100644 index 84060ddf29..0000000000 --- a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Internal definitions generated by :tacn:`abstract`\-like tactics are now inlined - inside universe :cmd:`Qed`\-terminated polymorphic definitions, similarly to what - happens for their monomorphic counterparts, - (`#10439 `_, by Pierre-Marie Pédrot). diff --git a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst deleted file mode 100644 index 5d224797d4..0000000000 --- a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Fixed:** - Section data is now part of the kernel. Solves a soundness issue - in interactive mode where global monomorphic universe constraints would be - dropped when forcing a delayed opaque proof inside a polymorphic section. Also - relaxes the nesting criterion for sections, as polymorphic sections can now - appear inside a monomorphic one - (`#10664, `_ by Pierre-Marie Pédrot). diff --git a/doc/changelog/01-kernel/10811-sprop-default-on.rst b/doc/changelog/01-kernel/10811-sprop-default-on.rst deleted file mode 100644 index 2c008fb5d3..0000000000 --- a/doc/changelog/01-kernel/10811-sprop-default-on.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - Using ``SProp`` is now allowed by default, without needing to pass - ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 - `_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10049-bidi-app.rst b/doc/changelog/02-specification-language/10049-bidi-app.rst deleted file mode 100644 index 024795f5da..0000000000 --- a/doc/changelog/02-specification-language/10049-bidi-app.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - Annotation in `Arguments` for bidirectionality hints: it is now possible - to tell type inference to use type information from the context once the `n` - first arguments of an application are known. The syntax is: - `Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)` - (`#10049 `_, by Maxime Dénès with - help from Enrico Tassi). diff --git a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst deleted file mode 100644 index 389ee4fd7f..0000000000 --- a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Record fields can be annotated to prevent them from being used as canonical projections; - see :ref:`canonicalstructures` for details - (`#10076 `_, - by Vincent Laporte). diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst deleted file mode 100644 index 87e4c9ff10..0000000000 --- a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst +++ /dev/null @@ -1,15 +0,0 @@ -- **Changed:** - Require parentheses around nested disjunctive patterns, so that pattern and - term syntax are consistent; match branch patterns no longer require - parentheses for notation at level 100 or more. - - .. warning:: Incompatibilities - - + In :g:`match p with (_, (0|1)) => ...` parentheses may no longer be - omitted around :n:`0|1`. - + Notation :g:`(p | q)` now potentially clashes with core pattern syntax, - and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. - - See :ref:`extendedpatternmatching` for details - (`#10167 `_, - by Georges Gonthier). diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst deleted file mode 100644 index c201b482e5..0000000000 --- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Changed:** - :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` - annotation, see :ref:`advanced-recursive-functions` for the updated - documentation (`#10215 `_, - by Enrico Tassi). - -- **Changed:** - The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used - inside a module type. In order to declare a module type parameter that - happens to be a morphism, use :cmd:`Declare Morphism`. See - :ref:`deprecated_syntax_for_generalized_rewriting` for the updated - documentation (`#10215 `_, - by Enrico Tassi). diff --git a/doc/changelog/02-specification-language/10441-static-poly-section.rst b/doc/changelog/02-specification-language/10441-static-poly-section.rst deleted file mode 100644 index 3d0ca000e6..0000000000 --- a/doc/changelog/02-specification-language/10441-static-poly-section.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Changed:** - The universe polymorphism setting now applies from the opening of a section. - In particular, it is not possible anymore to mix polymorphic and monomorphic - definitions in a section when there are no variables nor universe constraints - defined in this section. This makes the behaviour consistent with the - documentation. (`#10441 `_, - by Pierre-Marie Pédrot) - -- **Added:** - The :cmd:`Section` vernacular command now accepts the "universes" attribute. In - addition to setting the section universe polymorphism, it also locally sets - the universe polymorphic option inside the section. - (`#10441 `_, by Pierre-Marie Pédrot) diff --git a/doc/changelog/02-specification-language/10758-fix-10757.rst b/doc/changelog/02-specification-language/10758-fix-10757.rst deleted file mode 100644 index 431123ec1b..0000000000 --- a/doc/changelog/02-specification-language/10758-fix-10757.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes - involving ``Prop`` types (`#10758 - `_, by Gaëtan Gilbert, fixing - `#10757 `_ reported by - Xavier Leroy). diff --git a/doc/changelog/02-specification-language/10985-about-arguments.rst b/doc/changelog/02-specification-language/10985-about-arguments.rst deleted file mode 100644 index 0faaf95e6c..0000000000 --- a/doc/changelog/02-specification-language/10985-about-arguments.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Output of the :cmd:`Print` and :cmd:`About` commands. - Arguments meta-data is now displayed as the corresponding - :cmd:`Arguments ` command instead of the - human-targeted prose used in previous Coq versions. (`#10985 - `_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst deleted file mode 100644 index 51a62a0c8d..0000000000 --- a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more - predictable version of the old ``Refine Instance Mode`` which - unconditionally opens a proof (`#10996 - `_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst deleted file mode 100644 index 49f8f451a7..0000000000 --- a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - The unsupported attribute error is now an error-by-default warning, - meaning it can be disabled (`#10997 - `_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst deleted file mode 100644 index 6bf261eb9b..0000000000 --- a/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Fixed:** Bugs sometimes preventing to define valid (co)fixpoints with implicit arguments - in the presence of local definitions, see `#3282 `_ - (`#11132 `_, by Hugo Herbelin). - - .. example:: - - The following features an implicit argument after a local - definition. It was wrongly rejected. - - .. coqtop:: in - - Definition f := fix f (o := true) {n : nat} m {struct m} := - match m with 0 => 0 | S m' => f (n:=n+1) m' end. diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst deleted file mode 100644 index ed95a6eb4f..0000000000 --- a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Numeral Notations now support sorts in the input to printing - functions (e.g., numeral notations can be defined for terms - containing things like `@cons Set nat nil`). (`#9883 - `_, by Jason Gross). diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst deleted file mode 100644 index a3c185d5f1..0000000000 --- a/doc/changelog/03-notations/10180-deprecate-notations.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **Added:** - The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` - attribute - (`#10180 `_, by Maxime Dénès). - -- **Deprecated:** - The former `compat` annotation for notations is - deprecated, and its semantics changed. It is now made equivalent to using - a `deprecated` attribute, and is no longer connected with the `-compat` - command-line flag - (`#10180 `_, by Maxime Dénès). diff --git a/doc/changelog/03-notations/10963-simplify-parser.rst b/doc/changelog/03-notations/10963-simplify-parser.rst deleted file mode 100644 index 5dc0215225..0000000000 --- a/doc/changelog/03-notations/10963-simplify-parser.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - 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 `_, by Théo - Zimmermann, simplification initially noticed by Jim Fehrle). diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst deleted file mode 100644 index 0efae6902f..0000000000 --- a/doc/changelog/04-tactics/09288-injection-as.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Syntax :n:`injection @term as [= {+ @intropattern} ]` as - an alternative to :n:`injection @term as {+ @simple_intropattern}` using - the standard :n:`@injection_intropattern` syntax (`#9288 - `_, by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/09856-zify.rst b/doc/changelog/04-tactics/09856-zify.rst deleted file mode 100644 index c71a715ccc..0000000000 --- a/doc/changelog/04-tactics/09856-zify.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Changed:** - Reimplementation of the :tacn:`zify` tactic. The tactic is more efficient and copes with dependent hypotheses. - It can also be extended by redefining the tactic ``zify_post_hook``. - (`#9856 `_, fixes - `#8898 `_, - `#7886 `_, - `#9848 `_ and - `#5155 `_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/10318-select-only-error.rst b/doc/changelog/04-tactics/10318-select-only-error.rst deleted file mode 100644 index 3e4874dee6..0000000000 --- a/doc/changelog/04-tactics/10318-select-only-error.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - The goal selector tactical ``only`` now checks that the goal range - it is given is valid instead of ignoring goals out of the focus - range (`#10318 `_, by Gaëtan - Gilbert). diff --git a/doc/changelog/04-tactics/10765-micromega-caches.rst b/doc/changelog/04-tactics/10765-micromega-caches.rst deleted file mode 100644 index 82c14bcfdd..0000000000 --- a/doc/changelog/04-tactics/10765-micromega-caches.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. - (`#10765 `_, by Frédéric Besson, - see `#10772 `_ for use case). diff --git a/doc/changelog/04-tactics/10774-zify-Z_to_N.rst b/doc/changelog/04-tactics/10774-zify-Z_to_N.rst deleted file mode 100644 index 37a47a3c98..0000000000 --- a/doc/changelog/04-tactics/10774-zify-Z_to_N.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - The :tacn:`zify` tactic is now aware of `Z.to_N`. - (`#10774 `_, grants - `#9162 `_, by Kazuhiko Sakaguchi). diff --git a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst b/doc/changelog/04-tactics/10966-assert-succeeds-once.rst deleted file mode 100644 index 755febc39d..0000000000 --- a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Changed:** - The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now - only run their tactic argument once, even if it has multiple - successes. This prevents blow-up and looping from using - multisuccess tactics with :tacn:`assert_succeeds`. (`#10966 - `_ fixes `#10965 - `_, by Jason Gross). - -- **Fixed:** - The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now - behave correctly when their tactic fully solves the goal. (`#10966 - `_ fixes `#9114 - `_, by Jason Gross). diff --git a/doc/changelog/05-tactic-language/10002-ltac2.rst b/doc/changelog/05-tactic-language/10002-ltac2.rst deleted file mode 100644 index 8b910a4779..0000000000 --- a/doc/changelog/05-tactic-language/10002-ltac2.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Added:** - Ltac2, a new version of the tactic language Ltac, that doesn't - preserve backward compatibility, has been integrated in the main Coq - distribution. It is still experimental, but we already recommend - users of advanced Ltac to start using it and report bugs or request - enhancements. See its documentation in the :ref:`dedicated chapter - ` (`#10002 `_, plugin - authored by Pierre-Marie Pédrot, with contributions by various - users, integration by Maxime Dénès, help on integrating / improving - the documentation by Théo Zimmermann and Jim Fehrle). diff --git a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst deleted file mode 100644 index f32443cbb9..0000000000 --- a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Ltac2 tactic notations with “constr” arguments can specify the - interpretation scope for these arguments; - see :ref:`ltac2_notations` for details - (`#10289 `_, - by Vincent Laporte). diff --git a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst deleted file mode 100644 index 16ca9caf48..0000000000 --- a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - White spaces are forbidden in the :n:`&@ident` syntax for ltac2 references - that are described in :ref:`ltac2_built-in-quotations` - (`#10324 `_, - fixes `#10088 `_, - authored by Pierre-Marie Pédrot). diff --git a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst deleted file mode 100644 index 424540b46a..0000000000 --- a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst +++ /dev/null @@ -1,29 +0,0 @@ -- **Added:** - Generalize tactics :tacn:`under` and :tacn:`over` for any registered - relation. More precisely, assume the given context lemma has type - `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The - first step performed by :tacn:`under` (since Coq 8.10) amounts to - calling the tactic :tacn:`rewrite `, which - itself relies on :tacn:`setoid_rewrite` if need be. So this step was - already compatible with a double implication or setoid equality for - the conclusion head symbol `R2`. But a further step consists in - tagging the generated subgoal `R1 (f1 i) (?f2 i)` to protect it from - unwanted evar instantiation, and get `Under_rel _ R1 (f1 i) (?f2 i)` - that is displayed as ``'Under[ f1 i ]``. In Coq 8.10, this second - (convenience) step was only performed when `R1` was Leibniz' `eq` or - `iff`. Now, it is also performed for any relation `R1` which has a - ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance - being also needed so :tacn:`over` can discharge the ``'Under[ _ ]`` - goal by instantiating the hidden evar.) Also, it is now possible to - manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1` - is a `PreOrder` relation or so, thanks to extra instances proving - that `Under_rel` preserves the properties of the `R1` relation. - These two features generalizing support for setoid-like relations is - enabled as soon as we do both ``Require Import ssreflect.`` and - ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been - added if one wants to "unprotect" the evar, and instantiate it - manually with another rule than reflexivity (i.e., without using the - :tacn:`over` tactic nor the ``over`` rewrite rule). See also Section - :ref:`under_ssr` (`#10022 `_, - by Erik Martin-Dorel, with suggestions and review by Enrico Tassi - and Cyril Cohen). diff --git a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst deleted file mode 100644 index 1dbb3035ce..0000000000 --- a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - A :g:`void` notation for the standard library empty type (:g:`Empty_set`) - (`#10932 `_, by Arthur Azevedo de - Amorim). diff --git a/doc/changelog/06-ssreflect/11136-inj_compr.rst b/doc/changelog/06-ssreflect/11136-inj_compr.rst deleted file mode 100644 index 7ebf95b988..0000000000 --- a/doc/changelog/06-ssreflect/11136-inj_compr.rst +++ /dev/null @@ -1,2 +0,0 @@ -- **Added:** Lemma :g:`inj_compr` to :g:`ssr.ssrfun` - (`#11136 `_, by Cyril Cohen). diff --git a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst b/doc/changelog/07-commands-and-options/09530-rm-unknown.rst deleted file mode 100644 index cd94bb0513..0000000000 --- a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Removed:** - Deprecated flag `Refine Instance Mode` - (`#9530 `_, fixes - `#3632 `_, `#3890 - `_ and `#4638 - `_ - by Maxime Dénès, review by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst deleted file mode 100644 index 366f799c59..0000000000 --- a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Removed:** - Undocumented :n:`Instance : !@type` syntax - (`#10185 `_, by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/10277-no-show-script.rst b/doc/changelog/07-commands-and-options/10277-no-show-script.rst deleted file mode 100644 index ee870df607..0000000000 --- a/doc/changelog/07-commands-and-options/10277-no-show-script.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Removed:** - Deprecated ``Show Script`` command - (`#10277 `_, by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/10291-typing-flags.rst b/doc/changelog/07-commands-and-options/10291-typing-flags.rst deleted file mode 100644 index 7dc7def4b3..0000000000 --- a/doc/changelog/07-commands-and-options/10291-typing-flags.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Unsafe commands to enable/disable guard checking, positivity checking - and universes checking (providing a local `-type-in-type`). - See :ref:`controlling-typing-flags` - (`#10291 `_ by Simon Boulier). diff --git a/doc/changelog/07-commands-and-options/10476-fix-export.rst b/doc/changelog/07-commands-and-options/10476-fix-export.rst deleted file mode 100644 index af38008a88..0000000000 --- a/doc/changelog/07-commands-and-options/10476-fix-export.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Two bugs in :cmd:`Export`. This can have an impact on the behavior of the - :cmd:`Import` command on libraries. `Import A` when `A` imports `B` which exports - `C` was importing `C`, whereas :cmd:`Import` is not transitive. Also, after - `Import A B`, the import of `B` was sometimes incomplete. - (`#10476 `_, by Maxime Dénès). diff --git a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst b/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst deleted file mode 100644 index a17f1704fe..0000000000 --- a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Changed:** - Output generated by :flag:`Printing Dependent Evars Line` flag - used by the Prooftree tool in Proof General. - (`#10489 `_, - closes `#4504 `_, - `#10399 `_ and - `#10400 `_, - by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst deleted file mode 100644 index 69a9c40c3c..0000000000 --- a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - Optionally highlight the differences between successive proof steps in the - :cmd:`Show Proof` command. Experimental; only available in coqtop - and Proof General for now, may be supported in other IDEs - in the future. - (`#10494 `_, - by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/11187-remove-addpath.rst b/doc/changelog/07-commands-and-options/11187-remove-addpath.rst deleted file mode 100644 index 58c53e3b1d..0000000000 --- a/doc/changelog/07-commands-and-options/11187-remove-addpath.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** Legacy commands ``AddPath``, ``AddRecPath``, and ``DelPath`` - which were undocumented, broken variants of :cmd:`Add LoadPath`, - :cmd:`Add Rec LoadPath`, and :cmd:`Remove LoadPath` - (`#11187 `_, - by Maxime Dénès and Théo Zimmermann). diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst deleted file mode 100644 index 83937390fc..0000000000 --- a/doc/changelog/08-tools/08642-vos-files.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Added:** - `coqc` now provides the ability to generate compiled interfaces. - Use `coqc -vos foo.v` to skip all opaque proofs during the - compilation of `foo.v`, and output a file called `foo.vos`. - This feature is experimental. It enables working on a Coq file without the need to - first compile the proofs contained in its dependencies - (`#8642 `_ by Arthur Charguéraud, review by - Maxime Dénès and Emilio Gallego). diff --git a/doc/changelog/08-tools/10245-require-command-line.rst b/doc/changelog/08-tools/10245-require-command-line.rst deleted file mode 100644 index ca871bbf6b..0000000000 --- a/doc/changelog/08-tools/10245-require-command-line.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - Command-line options `-require-import`, `-require-export`, - `-require-import-from` and `-require-export-from`, as well as their - shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate - confusing command line option `-require` - (`#10245 `_ - by Hugo Herbelin, review by Emilio Gallego). diff --git a/doc/changelog/08-tools/10947-coq-makefile-dep.rst b/doc/changelog/08-tools/10947-coq-makefile-dep.rst deleted file mode 100644 index c59f1312d1..0000000000 --- a/doc/changelog/08-tools/10947-coq-makefile-dep.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Renamed `VDFILE` from `.coqdeps.d` to `..d` in the `coq_makefile` - utility, where `` is the name of the output file given by the - `-o` option. In this way two generated makefiles can coexist in the same - directory. - (`#10947 `_, by Kazuhiko Sakaguchi). diff --git a/doc/changelog/08-tools/11068-coqbin-noslash.rst b/doc/changelog/08-tools/11068-coqbin-noslash.rst deleted file mode 100644 index cd48f9d606..0000000000 --- a/doc/changelog/08-tools/11068-coqbin-noslash.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Fixed:** ``coq_makefile`` now supports environment variable ``COQBIN`` with - no ending ``/`` character (`#11068 - `_, by Gaëtan Gilbert). diff --git a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst deleted file mode 100644 index 4b9eb55cbd..0000000000 --- a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Moved the :tacn:`auto` hints of the `OrderedType` module into a new `ordered_type` - database - (`#9772 `_, - by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst b/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst deleted file mode 100644 index 8cfd826be0..0000000000 --- a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - Deprecated modules `Coq.ZArith.Zlogarithm` and `Coq.ZArith.Zsqrt_compat` - (`#9881 `_, - by Vincent Laporte). diff --git a/doc/changelog/10-standard-library/10445-constructive-reals.rst b/doc/changelog/10-standard-library/10445-constructive-reals.rst deleted file mode 100644 index 182f8a805c..0000000000 --- a/doc/changelog/10-standard-library/10445-constructive-reals.rst +++ /dev/null @@ -1,17 +0,0 @@ -- **Added:** - Module `Reals.ConstructiveCauchyReals` defines constructive real numbers - by Cauchy sequences of rational numbers - (`#10445 `_, by Vincent Semeria, - with the help and review of Guillaume Melquiond and Bas Spitters). - -- **Changed:** Classical real numbers are now defined - as a quotient of these constructive real numbers, which significantly reduces - the number of axioms needed (see `Reals.Rdefinitions` and `Reals.Raxioms`), - while preserving backward compatibility. - - Futhermore, the new axioms for classical real numbers include the limited - principle of omniscience (`sig_forall_dec`), which is a logical principle - instead of an *ad hoc* property of the real numbers. - - (`#10445 `_, by Vincent Semeria, - with the help and review of Guillaume Melquiond and Bas Spitters) diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst deleted file mode 100644 index 768fc46714..0000000000 --- a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Added:** - New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and - :g:`nth_error` functions on lists - (`#10651 `_, and - `#10731 `_, by Oliver Nash). - -- **Changed:** - The lemma :g:`filter_app` was moved to the :g:`List` module - (`#10651 `_, by Oliver Nash). diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst deleted file mode 100644 index 11efef4de0..0000000000 --- a/doc/changelog/10-standard-library/10827-dedekind-reals.rst +++ /dev/null @@ -1,12 +0,0 @@ -- **Added:** - 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. - - (`#10827 `_, by Vincent Semeria, - based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin, - code review by Hugo Herbelin). diff --git a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst deleted file mode 100644 index 8aef859ec8..0000000000 --- a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Standard equivalence between weak excluded-middle and the - classical instance of De Morgan's law, in module :g:`ClassicalFacts` - (`#10895 `_, by Hugo Herbelin). diff --git a/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst b/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst deleted file mode 100644 index 58038eab82..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Coq now officially supports OCaml 4.08. - See `INSTALL` file for details - (`#10471 `_, - by Emilio Jesús Gallego Arias). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 01db9da03b..9120f79012 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -6,6 +6,401 @@ Recent changes .. include:: ../unreleased.rst +Version 8.11 +------------ + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +Changes in 8.11+beta1 +~~~~~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Added:** + A built-in support of floating-point arithmetic, allowing + one to devise efficient reflection tactics involving numerical + computation. Primitive floats are added in the language of terms, + following the binary64 format of the IEEE 754 standard, and the + related operations are implemented for the different reduction + engines of Coq by using the corresponding processor operators in + rounding-to-nearest-even. The properties of these operators are + axiomatized in the theory :g:`Coq.Floats.FloatAxioms` which is part + of the library :g:`Coq.Floats.Floats`. + See Section :ref:`primitive-floats` + (`#9867 `_, + closes `#8276 `_, + by Guillaume Bertholon, Erik Martin-Dorel, Pierre Roux). +- **Changed:** + Internal definitions generated by :tacn:`abstract`\-like tactics are now inlined + inside universe :cmd:`Qed`\-terminated polymorphic definitions, similarly to what + happens for their monomorphic counterparts, + (`#10439 `_, by Pierre-Marie Pédrot). +- **Fixed:** + Section data is now part of the kernel. Solves a soundness issue + in interactive mode where global monomorphic universe constraints would be + dropped when forcing a delayed opaque proof inside a polymorphic section. Also + relaxes the nesting criterion for sections, as polymorphic sections can now + appear inside a monomorphic one + (`#10664, `_ by Pierre-Marie Pédrot). +- **Changed:** + Using ``SProp`` is now allowed by default, without needing to pass + ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 + `_, by Gaëtan Gilbert). + +**Specification language, type inference** + +- **Added:** + Annotation in `Arguments` for bidirectionality hints: it is now possible + to tell type inference to use type information from the context once the `n` + first arguments of an application are known. The syntax is: + `Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)` + (`#10049 `_, by Maxime Dénès with + help from Enrico Tassi). +- **Added:** + Record fields can be annotated to prevent them from being used as canonical projections; + see :ref:`canonicalstructures` for details + (`#10076 `_, + by Vincent Laporte). +- **Changed:** + Require parentheses around nested disjunctive patterns, so that pattern and + term syntax are consistent; match branch patterns no longer require + parentheses for notation at level 100 or more. + + .. warning:: Incompatibilities + + + In :g:`match p with (_, (0|1)) => ...` parentheses may no longer be + omitted around :n:`0|1`. + + Notation :g:`(p | q)` now potentially clashes with core pattern syntax, + and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. + + See :ref:`extendedpatternmatching` for details + (`#10167 `_, + by Georges Gonthier). +- **Changed:** + :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` + annotation, see :ref:`advanced-recursive-functions` for the updated + documentation (`#10215 `_, + by Enrico Tassi). +- **Changed:** + The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used + inside a module type. In order to declare a module type parameter that + happens to be a morphism, use :cmd:`Declare Morphism`. See + :ref:`deprecated_syntax_for_generalized_rewriting` for the updated + documentation (`#10215 `_, + by Enrico Tassi). +- **Changed:** + The universe polymorphism setting now applies from the opening of a section. + In particular, it is not possible anymore to mix polymorphic and monomorphic + definitions in a section when there are no variables nor universe constraints + defined in this section. This makes the behaviour consistent with the + documentation. (`#10441 `_, + by Pierre-Marie Pédrot) + +- **Added:** + The :cmd:`Section` vernacular command now accepts the "universes" attribute. In + addition to setting the section universe polymorphism, it also locally sets + the universe polymorphic option inside the section. + (`#10441 `_, by Pierre-Marie Pédrot) +- **Fixed:** + ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes + involving ``Prop`` types (`#10758 + `_, by Gaëtan Gilbert, fixing + `#10757 `_ reported by + Xavier Leroy). +- **Changed:** + Output of the :cmd:`Print` and :cmd:`About` commands. + Arguments meta-data is now displayed as the corresponding + :cmd:`Arguments ` command instead of the + human-targeted prose used in previous Coq versions. (`#10985 + `_, by Gaëtan Gilbert). +- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more + predictable version of the old ``Refine Instance Mode`` which + unconditionally opens a proof (`#10996 + `_, by Gaëtan Gilbert). +- **Changed:** + The unsupported attribute error is now an error-by-default warning, + meaning it can be disabled (`#10997 + `_, by Gaëtan Gilbert). +- **Fixed:** Bugs sometimes preventing to define valid (co)fixpoints with implicit arguments + in the presence of local definitions, see `#3282 `_ + (`#11132 `_, by Hugo Herbelin). + + .. example:: + + The following features an implicit argument after a local + definition. It was wrongly rejected. + + .. coqtop:: in + + Definition f := fix f (o := true) {n : nat} m {struct m} := + match m with 0 => 0 | S m' => f (n:=n+1) m' end. + +**Notations** + +- **Added:** + Numeral Notations now support sorts in the input to printing + functions (e.g., numeral notations can be defined for terms + containing things like `@cons Set nat nil`). (`#9883 + `_, by Jason Gross). +- **Added:** + The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` + attribute + (`#10180 `_, by Maxime Dénès). + +- **Deprecated:** + The former `compat` annotation for notations is + deprecated, and its semantics changed. It is now made equivalent to using + a `deprecated` attribute, and is no longer connected with the `-compat` + command-line flag + (`#10180 `_, by Maxime Dénès). +- **Changed:** + 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 `_, by Théo + Zimmermann, simplification initially noticed by Jim Fehrle). + +**Tactics** + +- **Added:** + Syntax :n:`injection @term as [= {+ @intropattern} ]` as + an alternative to :n:`injection @term as {+ @simple_intropattern}` using + the standard :n:`@injection_intropattern` syntax (`#9288 + `_, by Hugo Herbelin). +- **Changed:** + Reimplementation of the :tacn:`zify` tactic. The tactic is more efficient and copes with dependent hypotheses. + It can also be extended by redefining the tactic ``zify_post_hook``. + (`#9856 `_, fixes + `#8898 `_, + `#7886 `_, + `#9848 `_ and + `#5155 `_, by Frédéric Besson). +- **Changed:** + The goal selector tactical ``only`` now checks that the goal range + it is given is valid instead of ignoring goals out of the focus + range (`#10318 `_, by Gaëtan + Gilbert). +- **Added:** + Flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. + (`#10765 `_, by Frédéric Besson, + see `#10772 `_ for use case). +- **Added:** + The :tacn:`zify` tactic is now aware of `Z.to_N`. + (`#10774 `_, grants + `#9162 `_, by Kazuhiko Sakaguchi). +- **Changed:** + The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now + only run their tactic argument once, even if it has multiple + successes. This prevents blow-up and looping from using + multisuccess tactics with :tacn:`assert_succeeds`. (`#10966 + `_ fixes `#10965 + `_, by Jason Gross). +- **Fixed:** + The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now + behave correctly when their tactic fully solves the goal. (`#10966 + `_ fixes `#9114 + `_, by Jason Gross). + +**Tactic language** + +- **Added:** + Ltac2, a new version of the tactic language Ltac, that doesn't + preserve backward compatibility, has been integrated in the main Coq + distribution. It is still experimental, but we already recommend + users of advanced Ltac to start using it and report bugs or request + enhancements. See its documentation in the :ref:`dedicated chapter + ` (`#10002 `_, plugin + authored by Pierre-Marie Pédrot, with contributions by various + users, integration by Maxime Dénès, help on integrating / improving + the documentation by Théo Zimmermann and Jim Fehrle). +- **Added:** + Ltac2 tactic notations with “constr” arguments can specify the + interpretation scope for these arguments; + see :ref:`ltac2_notations` for details + (`#10289 `_, + by Vincent Laporte). +- **Changed:** + White spaces are forbidden in the :n:`&@ident` syntax for ltac2 references + that are described in :ref:`ltac2_built-in-quotations` + (`#10324 `_, + fixes `#10088 `_, + authored by Pierre-Marie Pédrot). + +**SSReflect** + +- **Added:** + Generalize tactics :tacn:`under` and :tacn:`over` for any registered + relation. More precisely, assume the given context lemma has type + `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The + first step performed by :tacn:`under` (since Coq 8.10) amounts to + calling the tactic :tacn:`rewrite `, which + itself relies on :tacn:`setoid_rewrite` if need be. So this step was + already compatible with a double implication or setoid equality for + the conclusion head symbol `R2`. But a further step consists in + tagging the generated subgoal `R1 (f1 i) (?f2 i)` to protect it from + unwanted evar instantiation, and get `Under_rel _ R1 (f1 i) (?f2 i)` + that is displayed as ``'Under[ f1 i ]``. In Coq 8.10, this second + (convenience) step was only performed when `R1` was Leibniz' `eq` or + `iff`. Now, it is also performed for any relation `R1` which has a + ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance + being also needed so :tacn:`over` can discharge the ``'Under[ _ ]`` + goal by instantiating the hidden evar.) Also, it is now possible to + manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1` + is a `PreOrder` relation or so, thanks to extra instances proving + that `Under_rel` preserves the properties of the `R1` relation. + These two features generalizing support for setoid-like relations is + enabled as soon as we do both ``Require Import ssreflect.`` and + ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been + added if one wants to "unprotect" the evar, and instantiate it + manually with another rule than reflexivity (i.e., without using the + :tacn:`over` tactic nor the ``over`` rewrite rule). See also Section + :ref:`under_ssr` (`#10022 `_, + by Erik Martin-Dorel, with suggestions and review by Enrico Tassi + and Cyril Cohen). +- **Added:** + A :g:`void` notation for the standard library empty type (:g:`Empty_set`) + (`#10932 `_, by Arthur Azevedo de + Amorim). +- **Added:** Lemma :g:`inj_compr` to :g:`ssr.ssrfun` + (`#11136 `_, by Cyril Cohen). + +**Commands and options** + +- **Removed:** + Deprecated flag `Refine Instance Mode` + (`#9530 `_, fixes + `#3632 `_, `#3890 + `_ and `#4638 + `_ + by Maxime Dénès, review by Gaëtan Gilbert). +- **Removed:** + Undocumented :n:`Instance : !@type` syntax + (`#10185 `_, by Gaëtan Gilbert). +- **Removed:** + Deprecated ``Show Script`` command + (`#10277 `_, by Gaëtan Gilbert). +- **Added:** + Unsafe commands to enable/disable guard checking, positivity checking + and universes checking (providing a local `-type-in-type`). + See :ref:`controlling-typing-flags` + (`#10291 `_ by Simon Boulier). +- **Fixed:** + Two bugs in :cmd:`Export`. This can have an impact on the behavior of the + :cmd:`Import` command on libraries. `Import A` when `A` imports `B` which exports + `C` was importing `C`, whereas :cmd:`Import` is not transitive. Also, after + `Import A B`, the import of `B` was sometimes incomplete. + (`#10476 `_, by Maxime Dénès). +- **Changed:** + Output generated by :flag:`Printing Dependent Evars Line` flag + used by the Prooftree tool in Proof General. + (`#10489 `_, + closes `#4504 `_, + `#10399 `_ and + `#10400 `_, + by Jim Fehrle). +- **Added:** + Optionally highlight the differences between successive proof steps in the + :cmd:`Show Proof` command. Experimental; only available in coqtop + and Proof General for now, may be supported in other IDEs + in the future. + (`#10494 `_, + by Jim Fehrle). +- **Removed:** Legacy commands ``AddPath``, ``AddRecPath``, and ``DelPath`` + which were undocumented, broken variants of :cmd:`Add LoadPath`, + :cmd:`Add Rec LoadPath`, and :cmd:`Remove LoadPath` + (`#11187 `_, + by Maxime Dénès and Théo Zimmermann). + +**Tools** + +- **Added:** + `coqc` now provides the ability to generate compiled interfaces. + Use `coqc -vos foo.v` to skip all opaque proofs during the + compilation of `foo.v`, and output a file called `foo.vos`. + This feature is experimental. It enables working on a Coq file without the need to + first compile the proofs contained in its dependencies + (`#8642 `_ by Arthur Charguéraud, review by + Maxime Dénès and Emilio Gallego). +- **Added:** + Command-line options `-require-import`, `-require-export`, + `-require-import-from` and `-require-export-from`, as well as their + shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate + confusing command line option `-require` + (`#10245 `_ + by Hugo Herbelin, review by Emilio Gallego). +- **Changed:** + Renamed `VDFILE` from `.coqdeps.d` to `..d` in the `coq_makefile` + utility, where `` is the name of the output file given by the + `-o` option. In this way two generated makefiles can coexist in the same + directory. + (`#10947 `_, by Kazuhiko Sakaguchi). +- **Fixed:** ``coq_makefile`` now supports environment variable ``COQBIN`` with + no ending ``/`` character (`#11068 + `_, by Gaëtan Gilbert). + +**Standard library** + +- **Changed:** + Moved the :tacn:`auto` hints of the `OrderedType` module into a new `ordered_type` + database + (`#9772 `_, + by Vincent Laporte). +- **Removed:** + Deprecated modules `Coq.ZArith.Zlogarithm` and `Coq.ZArith.Zsqrt_compat` + (`#9881 `_, + by Vincent Laporte). +- **Added:** + Module `Reals.ConstructiveCauchyReals` defines constructive real numbers + by Cauchy sequences of rational numbers + (`#10445 `_, by Vincent Semeria, + with the help and review of Guillaume Melquiond and Bas Spitters). + +- **Changed:** Classical real numbers are now defined + as a quotient of these constructive real numbers, which significantly reduces + the number of axioms needed (see `Reals.Rdefinitions` and `Reals.Raxioms`), + while preserving backward compatibility. + + Futhermore, the new axioms for classical real numbers include the limited + principle of omniscience (`sig_forall_dec`), which is a logical principle + instead of an *ad hoc* property of the real numbers. + + (`#10445 `_, by Vincent Semeria, + with the help and review of Guillaume Melquiond and Bas Spitters) +- **Added:** + 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. + + (`#10827 `_, by Vincent Semeria, + based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin, + code review by Hugo Herbelin). +- **Added:** + New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and + :g:`nth_error` functions on lists + (`#10651 `_, and + `#10731 `_, by Oliver Nash). +- **Changed:** + The lemma :g:`filter_app` was moved to the :g:`List` module + (`#10651 `_, by Oliver Nash). +- **Added:** + Standard equivalence between weak excluded-middle and the + classical instance of De Morgan's law, in module :g:`ClassicalFacts` + (`#10895 `_, by Hugo Herbelin). + +**Infrastructure and dependencies** + +- **Changed:** + Coq now officially supports OCaml 4.08. + See `INSTALL` file for details + (`#10471 `_, + by Emilio Jesús Gallego Arias). + Version 8.10 ------------ -- cgit v1.2.3