diff options
Diffstat (limited to 'doc')
63 files changed, 611 insertions, 324 deletions
diff --git a/doc/changelog/01-kernel/09867-floats.rst b/doc/changelog/01-kernel/09867-floats.rst deleted file mode 100644 index 56b5fc747a..0000000000 --- a/doc/changelog/01-kernel/09867-floats.rst +++ /dev/null @@ -1,13 +0,0 @@ -- A built-in support of floating-point arithmetic was added, 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 <https://github.com/coq/coq/pull/9867>`_, - closes `#8276 <https://github.com/coq/coq/issues/8276>`_, - by Guillaume Bertholon, Erik Martin-Dorel, Pierre Roux). diff --git a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md deleted file mode 100644 index e0573a2c74..0000000000 --- a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md +++ /dev/null @@ -1,4 +0,0 @@ -- Internal definitions generated by abstract-like tactics are now inlined - inside universe Qed-terminated polymorphic definitions, similarly to what - happens for their monomorphic counterparts, - (`#10439 <https://github.com/coq/coq/pull/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 bac08d12ea..0000000000 --- a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst +++ /dev/null @@ -1,6 +0,0 @@ -- 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, <https://github.com/coq/coq/pull/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 349c44c205..0000000000 --- a/doc/changelog/01-kernel/10811-sprop-default-on.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Using ``SProp`` is now allowed by default, without needing to pass - ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 - <https://github.com/coq/coq/pull/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 279bb9272a..0000000000 --- a/doc/changelog/02-specification-language/10049-bidi-app.rst +++ /dev/null @@ -1,6 +0,0 @@ -- New 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 <https://github.com/coq/coq/pull/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 0a902079b9..0000000000 --- a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Record fields can be annotated to prevent them from being used as canonical projections; - see :ref:`canonicalstructures` for details - (`#10076 <https://github.com/coq/coq/pull/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 2d17e569d3..0000000000 --- a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst +++ /dev/null @@ -1,12 +0,0 @@ -- 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. 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 <https://github.com/coq/coq/pull/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 71b10aaaf4..0000000000 --- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst +++ /dev/null @@ -1,11 +0,0 @@ -- :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` - annotation, see :ref:`advanced-recursive-functions` for the updated - documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, - by Enrico Tassi). - -- 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 <https://github.com/coq/coq/pull/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 7f0345d946..0000000000 --- a/doc/changelog/02-specification-language/10441-static-poly-section.rst +++ /dev/null @@ -1,11 +0,0 @@ -- 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 <https://github.com/coq/coq/pull/10441>`_, - by Pierre-Marie Pédrot) - -- 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 <https://github.com/coq/coq/pull/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 4cce26aedc..0000000000 --- a/doc/changelog/02-specification-language/10758-fix-10757.rst +++ /dev/null @@ -1,5 +0,0 @@ -- ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes - involving ``Prop`` types (`#10758 - <https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing - `#10757 <https://github.com/coq/coq/issues/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 1e05b0b0fe..0000000000 --- a/doc/changelog/02-specification-language/10985-about-arguments.rst +++ /dev/null @@ -1,5 +0,0 @@ -- The output of the :cmd:`Print` and :cmd:`About` commands has - changed. Arguments meta-data is now displayed as the corresponding - :cmd:`Arguments <Arguments (implicits)>` command instead of the - human-targeted prose used in previous Coq versions. (`#10985 - <https://github.com/coq/coq/pull/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 cd1a692f54..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 - <https://github.com/coq/coq/pull/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 43a748b365..0000000000 --- a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst +++ /dev/null @@ -1,3 +0,0 @@ -- The unsupported attribute error is now an error-by-default warning, - meaning it can be disabled (`#10997 - <https://github.com/coq/coq/pull/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 f8298cdbdd..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 <https://github.com/coq/coq/issues/3282>`_ - (`#11132 <https://github.com/coq/coq/pull/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 abc5a516ae..0000000000 --- a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst +++ /dev/null @@ -1,4 +0,0 @@ -- 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 - <https://github.com/coq/coq/pull/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 bce5db5865..0000000000 --- a/doc/changelog/03-notations/10180-deprecate-notations.rst +++ /dev/null @@ -1,6 +0,0 @@ -- The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` - attribute. 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 <https://github.com/coq/coq/pull/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 327a39bdb6..0000000000 --- a/doc/changelog/03-notations/10963-simplify-parser.rst +++ /dev/null @@ -1,6 +0,0 @@ -- 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/03-notations/11090-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst deleted file mode 100644 index 4423c2b587..0000000000 --- a/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Fixed an 8.10 regression related to the printing of coercions associated to notations - (`#11090 <https://github.com/coq/coq/pull/11090>`_, - fixes ` #11033 <https://github.com/coq/coq/issues/11033>`_, by Hugo Herbelin). diff --git a/doc/changelog/03-notations/11113-remove-compat.rst b/doc/changelog/03-notations/11113-remove-compat.rst new file mode 100644 index 0000000000..8c71d70cda --- /dev/null +++ b/doc/changelog/03-notations/11113-remove-compat.rst @@ -0,0 +1,4 @@ +- 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 new file mode 100644 index 0000000000..8551cf3aac --- /dev/null +++ b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst @@ -0,0 +1,2 @@ +- The printing algorithm now interleave 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/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst deleted file mode 100644 index 0cb669778c..0000000000 --- a/doc/changelog/04-tactics/09288-injection-as.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as - an alternative to :n:`injection @term as {+ @simple_intropattern}` using - the standard :n:`@injection_intropattern` syntax (`#9288 - <https://github.com/coq/coq/pull/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 6b9143c77b..0000000000 --- a/doc/changelog/04-tactics/09856-zify.rst +++ /dev/null @@ -1,7 +0,0 @@ -- 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 <https://github.com/coq/coq/pull/9856>`_ fixes - `#8898 <https://github.com/coq/coq/issues/8898>`_, - `#7886 <https://github.com/coq/coq/issues/7886>`_, - `#9848 <https://github.com/coq/coq/issues/9848>`_ and - `#5155 <https://github.com/coq/coq/issues/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 b4f991316e..0000000000 --- a/doc/changelog/04-tactics/10318-select-only-error.rst +++ /dev/null @@ -1,4 +0,0 @@ -- 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 <https://github.com/coq/coq/pull/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 12d8f68e63..0000000000 --- a/doc/changelog/04-tactics/10765-micromega-caches.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Introduction of flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. - (see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case) - (`#10765 <https://github.com/coq/coq/pull/10765>`_ fixes `#10772 <https://github.com/coq/coq/issues/10772>`_ , by Frédéric Besson). 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 ed46cb101e..0000000000 --- a/doc/changelog/04-tactics/10774-zify-Z_to_N.rst +++ /dev/null @@ -1,3 +0,0 @@ -- The :tacn:`zify` tactic is now aware of `Z.to_N`. - (`#10774 <https://github.com/coq/coq/pull/10774>`_ fixes - `#9162 <https://github.com/coq/coq/issues/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 09bef82c80..0000000000 --- a/doc/changelog/04-tactics/10966-assert-succeeds-once.rst +++ /dev/null @@ -1,11 +0,0 @@ -- 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 - <https://github.com/coq/coq/pull/10966>`_ fixes `#10965 - <https://github.com/coq/coq/issues/10965>`_, by Jason Gross). - -- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now - behave correctly when their tactic fully solves the goal. (`#10966 - <https://github.com/coq/coq/pull/10966>`_ fixes `#9114 - <https://github.com/coq/coq/issues/9114>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst index 3ec526f0a9..c72d085687 100644 --- a/doc/changelog/04-tactics/10998-zify-complements.rst +++ b/doc/changelog/04-tactics/10998-zify-complements.rst @@ -1,4 +1,5 @@ -- The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`, +- **Added:** + The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`, `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`, `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, and `Z.quot2`. Injections for internal definitions in module `ZifyBool` (`isZero` and `isLeZero`) 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 6d62f11eff..0000000000 --- a/doc/changelog/05-tactic-language/10002-ltac2.rst +++ /dev/null @@ -1,9 +0,0 @@ -- 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 - <ltac2>` (`#10002 <https://github.com/coq/coq/pull/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 bd1c0c42e8..0000000000 --- a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Ltac2 tactic notations with “constr” arguments can specify the - interpretation scope for these arguments; - see :ref:`ltac2_notations` for details - (`#10289 <https://github.com/coq/coq/pull/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 fba09f5e87..0000000000 --- a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst +++ /dev/null @@ -1,5 +0,0 @@ -- White spaces are forbidden in the “&ident” syntax for ltac2 references - that are described in :ref:`ltac2_built-in-quotations` - (`#10324 <https://github.com/coq/coq/pull/10324>`_, - fixes `#10088 <https://github.com/coq/coq/issues/10088>`_, - authored by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst b/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst new file mode 100644 index 0000000000..462ba4a7b1 --- /dev/null +++ b/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Syntax of tactic `cofix ... with ...` was broken from Coq 8.10. + (`#11241 <https://github.com/coq/coq/pull/11241>`_, + by Hugo Herbelin). 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 5e005742fd..0000000000 --- a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst +++ /dev/null @@ -1,28 +0,0 @@ -- 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 <rewrite (ssreflect)>`, 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 <https://github.com/coq/coq/pull/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 7366ef1190..0000000000 --- a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Add a :g:`void` notation for the standard library empty type (:g:`Empty_set`) - (`#10932 <https://github.com/coq/coq/pull/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 b546fcde6b..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 <https://github.com/coq/coq/pull/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 1c91800c65..0000000000 --- a/doc/changelog/07-commands-and-options/09530-rm-unknown.rst +++ /dev/null @@ -1,6 +0,0 @@ -- Deprecated flag `Refine Instance Mode` has been removed. - (`#9530 <https://github.com/coq/coq/pull/9530>`_, fixes - `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890 - <https://github.com/coq/coq/issues/3890>`_ and `#4638 - <https://github.com/coq/coq/issues/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 c69cda9656..0000000000 --- a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst +++ /dev/null @@ -1,2 +0,0 @@ -- Remove undocumented :n:`Instance : !@type` syntax - (`#10185 <https://github.com/coq/coq/pull/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 7fdeb632b4..0000000000 --- a/doc/changelog/07-commands-and-options/10277-no-show-script.rst +++ /dev/null @@ -1,2 +0,0 @@ -- Remove ``Show Script`` command (deprecated since 8.10) - (`#10277 <https://github.com/coq/coq/pull/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 ef7adde801..0000000000 --- a/doc/changelog/07-commands-and-options/10291-typing-flags.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Adding unsafe commands to enable/disable guard checking, positivity checking - and universes checking (providing a local `-type-in-type`). - See :ref:`controlling-typing-flags`. - (`#10291 <https://github.com/coq/coq/pull/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 ba71e1c337..0000000000 --- a/doc/changelog/07-commands-and-options/10476-fix-export.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Fix two bugs in `Export`. This can have an impact on the behavior of the - `Import` command on libraries. `Import A` when `A` imports `B` which exports - `C` was importing `C`, whereas `Import` is not transitive. Also, after - `Import A B`, the import of `B` was sometimes incomplete. - (`#10476 <https://github.com/coq/coq/pull/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 580e808baa..0000000000 --- a/doc/changelog/07-commands-and-options/10489-print_dependent_evars.rst +++ /dev/null @@ -1,7 +0,0 @@ -- Update output generated by :flag:`Printing Dependent Evars Line` flag - used by the Prooftree tool in Proof General. - (`#10489 <https://github.com/coq/coq/pull/10489>`_, - closes `#4504 <https://github.com/coq/coq/issues/4504>`_, - `#10399 <https://github.com/coq/coq/issues/10399>`_ and - `#10400 <https://github.com/coq/coq/issues/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 c1df728c5c..0000000000 --- a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst +++ /dev/null @@ -1,6 +0,0 @@ -- 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 <https://github.com/coq/coq/pull/10494>`_, - by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/11162-local-cs.rst b/doc/changelog/07-commands-and-options/11162-local-cs.rst new file mode 100644 index 0000000000..5a69a107cd --- /dev/null +++ b/doc/changelog/07-commands-and-options/11162-local-cs.rst @@ -0,0 +1 @@ +- 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/11185-remove-typeclasses-axioms-instances.rst b/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst new file mode 100644 index 0000000000..9fc09c4189 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst @@ -0,0 +1,3 @@ +- **Removed:** ``Typeclasses Axioms Are Instances`` flag, deprecated since 8.10. + Use :cmd:`Declare Instance` for axioms which should be instances + (`#11185 <https://github.com/coq/coq/pull/11185>`_, by 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 f612096880..0000000000 --- a/doc/changelog/08-tools/08642-vos-files.rst +++ /dev/null @@ -1,7 +0,0 @@ -- `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 <https://github.com/coq/coq/pull/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 54417077f5..0000000000 --- a/doc/changelog/08-tools/10245-require-command-line.rst +++ /dev/null @@ -1,6 +0,0 @@ -- Add 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 <https://github.com/coq/coq/pull/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 f620b32cb8..0000000000 --- a/doc/changelog/08-tools/10947-coq-makefile-dep.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` - utility, where `<CoqMakefile>` 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 <https://github.com/coq/coq/pull/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 c2c8f4df31..0000000000 --- a/doc/changelog/08-tools/11068-coqbin-noslash.rst +++ /dev/null @@ -1,3 +0,0 @@ -- ``coq_makefile`` now supports environment variable ``COQBIN`` with - no ending ``/`` character (`#11068 - <https://github.com/coq/coq/pull/11068>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst new file mode 100644 index 0000000000..ecc134748d --- /dev/null +++ b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst @@ -0,0 +1,4 @@ +- **Fixed:** + ``coqtop --version`` was broken when called in the middle of an installation process + (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing + `#11254 <https://github.com/coq/coq/pull/11254>`_). 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 7babcdb6f1..0000000000 --- a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Moved the `auto` hints of the `OrderedType` module into a new `ordered_type` - database - (`#9772 <https://github.com/coq/coq/pull/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 ab625b9e03..0000000000 --- a/doc/changelog/10-standard-library/09811-remove-zlogarithm.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Removes deprecated modules `Coq.ZArith.Zlogarithm` - and `Coq.ZArith.Zsqrt_compat` - (#9881 <https://github.com/coq/coq/pull/9811> - 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 d69056fc2f..0000000000 --- a/doc/changelog/10-standard-library/10445-constructive-reals.rst +++ /dev/null @@ -1,12 +0,0 @@ -- New module `Reals.ConstructiveCauchyReals` defines constructive real numbers - by Cauchy sequences of rational numbers. 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. - - See `#10445 <https://github.com/coq/coq/pull/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 864c4e6a7e..0000000000 --- a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst +++ /dev/null @@ -1,6 +0,0 @@ -- New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and - :g:`nth_error` functions on lists. The lemma :g:`filter_app` was moved to the - :g:`List` module. - - See `#10651 <https://github.com/coq/coq/pull/10651>`_, and - `#10731 <https://github.com/coq/coq/pull/10731>`_, 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 5d8467025b..0000000000 --- a/doc/changelog/10-standard-library/10827-dedekind-reals.rst +++ /dev/null @@ -1,11 +0,0 @@ -- 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/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 6e87ff93c7..0000000000 --- a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst +++ /dev/null @@ -1 +0,0 @@ -- ClassicalFacts: Adding the standard equivalence between weak excluded-middle and the classical instance of De Morgan's law (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin). diff --git a/doc/changelog/10-standard-library/11127-trunk.rst b/doc/changelog/10-standard-library/11127-trunk.rst new file mode 100644 index 0000000000..ef1d41d17f --- /dev/null +++ b/doc/changelog/10-standard-library/11127-trunk.rst @@ -0,0 +1,2 @@ +- **Added:** theorem :g:`bezout_comm` for natural numbers + (`#11127 <https://github.com/coq/coq/pull/11127>`_, by Daniel de Rauglaudre). 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 8bfd01d7a0..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/10471-ocaml-408.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Coq now officially supports OCaml 4.08. - - see INSTALL files for details - (`#10471 <https://github.com/coq/coq/pull/10471>`_, - by Emilio Jesús Gallego Arias). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst b/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst new file mode 100644 index 0000000000..5c08e2b0ea --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst @@ -0,0 +1,5 @@ +- **Added:** + Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` + environment variable + (`#11227 <https://github.com/coq/coq/pull/11227>`_, + by Bernhard M. Wiedemann). diff --git a/doc/changelog/README.md b/doc/changelog/README.md index 3e0970a656..05bf710f89 100644 --- a/doc/changelog/README.md +++ b/doc/changelog/README.md @@ -15,12 +15,12 @@ entry in [`dev/doc/changes.md`](../../dev/doc/changes.md). ## How to add an entry? ## Run `./dev/tools/make-changelog.sh`: it will ask you for your PR -number, and to choose among the predefined categories. Afterward, -fill in the automatically generated entry with a short description of -your change (which should describe any compatibility issues in -particular). You may also add a reference to the relevant fixed -issue, and credit reviewers, co-authors, and anyone who helped advance -the PR. +number, and to choose among the predefined categories, and the +predefined types of changes. Afterward, fill in the automatically +generated entry with a short description of your change (which should +describe any compatibility issues in particular). You may also add a +reference to the relevant fixed issue, and credit reviewers, +co-authors, and anyone who helped advance the PR. The format for changelog entries is the same as in the reference manual. In particular, you may reference the documentation you just @@ -31,10 +31,18 @@ manual for details. Here is a summary of the structure of a changelog entry: ``` rst -- Description of the changes, with possible link to +- **Added / Changed / Deprecated / Fixed / Removed:** + 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 first line indicates the type of change. Available types come +from the [Keep a Changelog +1.0.0](https://keepachangelog.com/en/1.0.0/) specification. We +exclude the "Security" type for now because of the absence of a +process for handling critical bugs (proof of False) as security +vulnerabilities. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 661aa88082..57a2254100 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -576,14 +576,6 @@ Settings of goals. Setting this option to 1 or 2 turns on the :flag:`Typeclasses Debug` flag; setting this option to 0 turns that flag off. -.. flag:: Typeclasses Axioms Are Instances - - .. deprecated:: 8.10 - - This flag (off by default since 8.8) automatically declares axioms - whose type is a typeclass at declaration time as instances of that - class. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 80a24b997c..1d0c937792 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -6,6 +6,512 @@ Recent changes .. include:: ../unreleased.rst +Version 8.11 +------------ + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +The main changes brought by |Coq| version 8.11 are: + +- `Ltac2`__, a new tactic language for writing more robust larger scale + tactics, with built-in support for datatypes and the multi-goal tactic monad. +- `Primitive floats`__ are integrated in terms and follow the binary64 format + of the IEEE 754 standard, as specified in the `Coq.Float.Floats` library. +- `Cleanups`__ of the section mechanism, delayed proofs and further + restrictions of template polymorphism to fix soundness issues related to + universes. +- New `unsafe flags`__ to disable locally guard, positivity and universe + checking. Reliance on these flags is always printed by + :g:`Print Assumptions`. +- `Fixed bugs`__ of :g:`Export` and :g:`Import` that can have a + significant impact on user developments (**common source of + incompatibility!**). +- New interactive development method based on `vos` `interface files`__, + allowing to work on a file without recompiling the proof parts of their + dependencies. +- New :g:`Arguments` annotation for `bidirectional type inference`__ + configuration for reference (e.g. constants, inductive) applications. +- New `refine attribute`__ for :cmd:`Instance` can be used instead of + the removed ``Refine Instance Mode``. +- Generalization of the :g:`under` and :g:`over` tactics__ of SSReflect to + arbitrary relations. +- `Revision`__ of the :g:`Coq.Reals` library, its axiomatisation and + instances of the constructive and classical real numbers. + +__ 811Ltac2_ +__ 811PrimitiveFloats_ +__ 811Sections_ +__ 811UnsafeFlags_ +__ 811ExportBug_ +__ 811vos_ +__ 811BidirArguments_ +__ 811RefineInstance_ +__ 811SSRUnderOver_ +__ 811Reals_ + +The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq| +and affected releases. See the `Changes in 8.11+beta1`_ section for the +detailed list of changes, including potentially breaking changes marked with +**Changed**. + +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop, Théo Zimmermann worked on maintaining and improving the +continuous integration system and package building infrastructure. + +Coq's documentation is available at https://coq.github.io/doc/V8.11+beta1/api (documentation of +the ML API), https://coq.github.io/doc/V8.11+beta1/refman (reference +manual), and https://coq.github.io/doc/V8.11+beta1/stdlib (documentation of +the standard library). + +The OPAM repository for |Coq| packages has been maintained by +Karl Palmskog, Matthieu Sozeau, Enrico Tassi with contributions +from many users. A list of packages is available at +https://coq.inria.fr/opam/www/. + +The 61 contributors to this version are Michael D. Adams, Guillaume +Allais, Helge Bahmann, Langston Barrett, Guillaume Bertholon, Frédéric +Besson, Simon Boulier, Michele Caci, Tej Chajed, Arthur Charguéraud, +Cyril Cohen, Frédéric Dabrowski, Arthur Azevedo de Amorim, Maxime +Dénès, Nikita Eshkeev, Jim Fehrle, Emilio Jesús Gallego Arias, +Paolo G. Giarrusso, Gaëtan Gilbert, Georges Gonthier, Jason Gross, +Samuel Gruetter, Armaël Guéneau, Hugo Herbelin, Florent Hivert, Jasper +Hugunin, Shachar Itzhaky, Jan-Oliver Kaiser, Robbert Krebbers, Vincent +Laporte, Olivier Laurent, Samuel Lelièvre, Nicholas Lewycky, Yishuai +Li, Jose Fernando Lopez Fernandez, Andreas Lynge, Kenji Maillard, Erik +Martin-Dorel, Guillaume Melquiond, Alexandre Moine, Oliver Nash, +Wojciech Nawrocki, Antonio Nikishaev, Pierre-Marie Pédrot, Clément +Pit-Claudel, Lars Rasmusson, Robert Rand, Talia Ringer, JP Rodi, +Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, +Matthieu Sozeau, spanjel, Claude Stolze, Enrico Tassi, Laurent Théry, +James R. Wilcox, Xia Li-yao, Théo Zimmermann + +Many power users helped to improve the design of the new features via +the issue and pull request system, the |Coq| development mailing list, +the coq-club@inria.fr mailing list or the `Discourse forum +<https://coq.discourse.group/>`_. It would be impossible to mention +exhaustively the names of everybody who to some extent influenced the +development. + +Version 8.11 is the sixth release of |Coq| developed on a time-based +development cycle. Its development spanned 3 months from the release of +|Coq| 8.10. Pierre-Marie Pédrot is the release manager and maintainer of this +release, assisted by Matthieu Sozeau. This release is the result of 2000+ +commits and 300+ PRs merged, closing 75+ issues. + +| Paris, November 2019, +| Matthieu Sozeau for the |Coq| development team +| + + +Changes in 8.11+beta1 +~~~~~~~~~~~~~~~~~~~~~ + +**Kernel** + + .. _811PrimitiveFloats: + +- **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 <https://github.com/coq/coq/pull/9867>`_, + closes `#8276 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot). + + .. _811Sections: + +- **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, <https://github.com/coq/coq/pull/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 + <https://github.com/coq/coq/pull/10811>`_, by Gaëtan Gilbert). + +**Specification language, type inference** + + .. _811BidirArguments: + +- **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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) +- **Fixed:** + ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes + involving ``Prop`` types (`#10758 + <https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing + `#10757 <https://github.com/coq/coq/issues/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 <Arguments (implicits)>` command instead of the + human-targeted prose used in previous Coq versions. (`#10985 + <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). + + .. _811RefineInstance: + +- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more + predictable version of the old ``Refine Instance Mode`` which + unconditionally opens a proof (`#10996 + <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert). +- **Changed:** + The unsupported attribute error is now an error-by-default warning, + meaning it can be disabled (`#10997 + <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/issues/3282>`_ + (`#11132 <https://github.com/coq/coq/pull/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 + <https://github.com/coq/coq/pull/9883>`_, by Jason Gross). +- **Added:** + The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` + attribute + (`#10180 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/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 + <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/9856>`_, fixes + `#8898 <https://github.com/coq/coq/issues/8898>`_, + `#7886 <https://github.com/coq/coq/issues/7886>`_, + `#9848 <https://github.com/coq/coq/issues/9848>`_ and + `#5155 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan + Gilbert). +- **Added:** + Flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. + (`#10765 <https://github.com/coq/coq/pull/10765>`_, by Frédéric Besson, + see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case). +- **Added:** + The :tacn:`zify` tactic is now aware of `Z.to_N`. + (`#10774 <https://github.com/coq/coq/pull/10774>`_, grants + `#9162 <https://github.com/coq/coq/issues/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 + <https://github.com/coq/coq/pull/10966>`_ fixes `#10965 + <https://github.com/coq/coq/issues/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 + <https://github.com/coq/coq/pull/10966>`_ fixes `#9114 + <https://github.com/coq/coq/issues/9114>`_, by Jason Gross). + +**Tactic language** + + .. _811Ltac2: + +- **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 + <ltac2>` (`#10002 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/10324>`_, + fixes `#10088 <https://github.com/coq/coq/issues/10088>`_, + authored by Pierre-Marie Pédrot). + +**SSReflect** + + .. _811SSRUnderOver: + +- **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 <rewrite (ssreflect)>`, 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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/10932>`_, by Arthur Azevedo de + Amorim). +- **Added:** Lemma :g:`inj_compr` to :g:`ssr.ssrfun` + (`#11136 <https://github.com/coq/coq/pull/11136>`_, by Cyril Cohen). + +**Commands and options** + +- **Removed:** + Deprecated flag `Refine Instance Mode` + (`#9530 <https://github.com/coq/coq/pull/9530>`_, fixes + `#3632 <https://github.com/coq/coq/issues/3632>`_, `#3890 + <https://github.com/coq/coq/issues/3890>`_ and `#4638 + <https://github.com/coq/coq/issues/4638>`_ + by Maxime Dénès, review by Gaëtan Gilbert). +- **Removed:** + Undocumented :n:`Instance : !@type` syntax + (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). +- **Removed:** + Deprecated ``Show Script`` command + (`#10277 <https://github.com/coq/coq/pull/10277>`_, by Gaëtan Gilbert). + + .. _811UnsafeFlags: + +- **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 <https://github.com/coq/coq/pull/10291>`_ by Simon Boulier). + + .. _811ExportBug: + +- **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 <https://github.com/coq/coq/pull/10476>`_, by Maxime Dénès). + + .. warning:: + + This is a common source of incompatibilities in projects + migrating to Coq 8.11. + +- **Changed:** + Output generated by :flag:`Printing Dependent Evars Line` flag + used by the Prooftree tool in Proof General. + (`#10489 <https://github.com/coq/coq/pull/10489>`_, + closes `#4504 <https://github.com/coq/coq/issues/4504>`_, + `#10399 <https://github.com/coq/coq/issues/10399>`_ and + `#10400 <https://github.com/coq/coq/issues/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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/11187>`_, + by Maxime Dénès and Théo Zimmermann). + +**Tools** + + .. _811vos: + +- **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 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/10245>`_ + by Hugo Herbelin, review by Emilio Gallego). +- **Changed:** + Renamed `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the `coq_makefile` + utility, where `<CoqMakefile>` 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 <https://github.com/coq/coq/pull/10947>`_, by Kazuhiko Sakaguchi). +- **Fixed:** ``coq_makefile`` now supports environment variable ``COQBIN`` with + no ending ``/`` character (`#11068 + <https://github.com/coq/coq/pull/11068>`_, by Gaëtan Gilbert). + +**Standard library** + +- **Changed:** + Moved the :tacn:`auto` hints of the `OrderedType` module into a new `ordered_type` + database + (`#9772 <https://github.com/coq/coq/pull/9772>`_, + by Vincent Laporte). +- **Removed:** + Deprecated modules `Coq.ZArith.Zlogarithm` and `Coq.ZArith.Zsqrt_compat` + (`#9881 <https://github.com/coq/coq/pull/9811>`_, + by Vincent Laporte). + + .. _811Reals: + +- **Added:** + Module `Reals.ConstructiveCauchyReals` defines constructive real numbers + by Cauchy sequences of rational numbers + (`#10445 <https://github.com/coq/coq/pull/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-valued 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` now corresponds to these Dedekind reals, + hidden behind an opaque module, which significantly reduces the + number of axioms needed (see `Reals.Rdefinitions` and + `Reals.Raxioms`), while preserving backward compatibility. + Classical Dedekind reals are a quotient of constructive reals, which + allows to transport many constructive proofs to the classical case + (`#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). +- **Added:** + New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and + :g:`nth_error` functions on lists + (`#10651 <https://github.com/coq/coq/pull/10651>`_, and + `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash). +- **Changed:** + The lemma :g:`filter_app` was moved to the :g:`List` module + (`#10651 <https://github.com/coq/coq/pull/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 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin). + +**Infrastructure and dependencies** + +- **Changed:** + Coq now officially supports OCaml 4.08. + See `INSTALL` file for details + (`#10471 <https://github.com/coq/coq/pull/10471>`_, + by Emilio Jesús Gallego Arias). + Version 8.10 ------------ @@ -568,7 +1074,7 @@ Other changes in 8.10+beta1 - The prelude used to be automatically Exported and is now only Imported. This should be relevant only when importing files which don't use `-noinit` into files which do - (`#9013 <https://github.com/coq/coq/pull/9013>`_, by Gaëtan Gilert). + (`#9013 <https://github.com/coq/coq/pull/9013>`_, by Gaëtan Gilbert). - Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an ordered type, using lexical order @@ -765,6 +1271,51 @@ A few bug fixes and documentation improvements, in particular: fixes `#4741 <https://github.com/coq/coq/issues/4741>`_, by Helge Bahmann). +Changes in 8.10.2 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- Fixed a critical bug of template polymorphism and nonlinear universes + (`#11128 <https://github.com/coq/coq/pull/11128>`_, + fixes `#11039 <https://github.com/coq/coq/issues/11039>`_, + by Gaëtan Gilbert). + +- Fixed an anomaly “Uncaught exception Constr.DestKO” on :g:`Inductive` + (`#11052 <https://github.com/coq/coq/pull/11052>`_, + fixes `#11048 <https://github.com/coq/coq/issues/11048>`_, + by Gaëtan Gilbert). + +- Fixed an anomaly “not enough abstractions in fix body” + (`#11014 <https://github.com/coq/coq/pull/11014>`_, + fixes `#8459 <https://github.com/coq/coq/issues/8459>`_, + by Gaëtan Gilbert). + +**Notations** + +- Fixed an 8.10 regression related to the printing of coercions associated to notations + (`#11090 <https://github.com/coq/coq/pull/11090>`_, + fixes `#11033 <https://github.com/coq/coq/issues/11033>`_, by Hugo Herbelin). + +**CoqIDE** + +- Fixed uneven dimensions of CoqIDE panels when window has been resized + (`#11070 <https://github.com/coq/coq/pull/11070>`_, + fixes 8.10-regression `#10956 <https://github.com/coq/coq/issues/10956>`_, + by Guillaume Melquiond). + +- Do not include final stops in queries + (`#11069 <https://github.com/coq/coq/pull/11069>`_, + fixes 8.10-regression `#11058 <https://github.com/coq/coq/issues/11058>`_, + by Guillaume Melquiond). + +**Infrastructure and dependencies** + +- Enable building of executables when they are running + (`#11000 <https://github.com/coq/coq/pull/11000>`_, + fixes 8.9-regression `#10728 <https://github.com/coq/coq/issues/10728>`_, + by Gaëtan Gilbert). + Version 8.9 ----------- diff --git a/doc/sphinx/dune b/doc/sphinx/dune index 353d58c676..b788fbbeed 100644 --- a/doc/sphinx/dune +++ b/doc/sphinx/dune @@ -1,8 +1,10 @@ (dirs :standard _static) -(rule (targets README.gen.rst) +(rule + (targets README.gen.rst) (deps (source_tree ../tools/coqrst) README.template.rst) (action (run ../tools/coqrst/regen_readme.py %{targets}))) -(alias (name refman-html) - (action (diff README.rst README.gen.rst))) +(rule + (alias refman-html) + (action (diff README.rst README.gen.rst))) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ae0afc7819..8caa289a47 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2003,10 +2003,11 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -.. cmd:: Canonical {? Structure } @qualid +.. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid This command declares :token:`qualid` as a canonical instance of a - structure (a record). + structure (a record). When the :g:`#[local]` attribute is given the effect + stops at the end of the :g:`Section` containig it. Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -2069,7 +2070,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. See :ref:`canonicalstructures` for a more realistic example. - .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term + .. cmdv:: {? Local | #[local] } Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the declaration :n:`Canonical @ident`. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 4f903d5776..81e50c0834 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2824,11 +2824,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: cutrewrite <- (@term = @term’) :name: cutrewrite - This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as <-`. + .. deprecated:: 8.5 + + This tactic can be replaced by :n:`enough (@term = @term’) as <-`. .. tacv:: cutrewrite -> (@term = @term’) - This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as ->`. + .. deprecated:: 8.5 + + This tactic can be replaced by :n:`enough (@term = @term’) as ->`. .. tacn:: subst @ident @@ -4895,6 +4899,8 @@ Performance-oriented tactic variants .. tacv:: convert_concl_no_check @term :name: convert_concl_no_check + .. deprecated:: 8.11 + Deprecated old name for :tacn:`change_no_check`. Does not support any of its variants. |