diff options
160 files changed, 1298 insertions, 963 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 87101ecae7..e8244fafc8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -6,6 +6,7 @@ stages: - stage-2 # Only dependencies in stage 1 - stage-3 # Only dependencies in stage 1 and 2 - stage-4 # Only dependencies in stage 1, 2 and 3 + - stage-5 # Only dependencies in stage 1, 2, 3, and 4 - deploy # When a job has no dependencies, it goes to stage 1. Otherwise, we @@ -704,12 +705,13 @@ library:ci-engine_bench: library:ci-fcsl_pcm: extends: .ci-template -# We cannot use flambda due to -# https://github.com/ocaml/ocaml/issues/7842, see -# https://github.com/coq/coq/pull/11916#issuecomment-609977375 library:ci-fiat_crypto: - extends: .ci-template + extends: .ci-template-flambda stage: stage-4 + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci needs: - build:edge+flambda - library:ci-coqprime @@ -720,6 +722,19 @@ library:ci-fiat_crypto: - library:ci-coqprime - plugin:ci-rewriter +# We cannot use flambda due to +# https://github.com/ocaml/ocaml/issues/7842, see +# https://github.com/coq/coq/pull/11916#issuecomment-609977375 +library:ci-fiat_crypto_ocaml: + extends: .ci-template + stage: stage-5 + needs: + - build:edge+flambda + - library:ci-fiat_crypto + dependencies: + - build:edge+flambda + - library:ci-fiat_crypto + library:ci-flocq: extends: .ci-template-flambda artifacts: diff --git a/Makefile.ci b/Makefile.ci index 9b7008f765..9231fa6fed 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -28,6 +28,7 @@ CI_TARGETS= \ ci-equations \ ci-fcsl_pcm \ ci-fiat_crypto \ + ci-fiat_crypto_ocaml \ ci-fiat_parsers \ ci-flocq \ ci-geocoq \ @@ -72,6 +73,7 @@ ci-corn: ci-math_classes ci-mtac2: ci-unicoq ci-fiat_crypto: ci-coqprime ci-rewriter +ci-fiat_crypto_ocaml: ci-fiat_crypto ci-simple_io: ci-ext_lib ci-quickchick: ci-ext_lib ci-simple_io diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh index 811fefda35..3ecdb32a51 100755 --- a/dev/ci/ci-fiat_crypto.sh +++ b/dev/ci/ci-fiat_crypto.sh @@ -15,8 +15,8 @@ fiat_crypto_CI_STACKSIZE=32768 # bedrock2, so we use the pinned version of bedrock2, but the external # version of other developments fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1" -fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite" -fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all" +fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} pre-standalone-extracted printlite lite" +fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all-except-compiled" ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ ulimit -s ${fiat_crypto_CI_STACKSIZE} && \ diff --git a/dev/ci/ci-fiat_crypto_ocaml.sh b/dev/ci/ci-fiat_crypto_ocaml.sh new file mode 100755 index 0000000000..20d3deb14f --- /dev/null +++ b/dev/ci/ci-fiat_crypto_ocaml.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1" + +( cd "${CI_BUILD_DIR}/fiat_crypto" && make ${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml lite-generated-files ) diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh index e1aed4560d..de58527cca 100755 --- a/dev/tools/make-changelog.sh +++ b/dev/tools/make-changelog.sh @@ -25,11 +25,17 @@ case "$type_first_letter" in exit 1;; esac +printf "Fixes? (space separated list of bug numbers)\n" +read -r fixes_list + +fixes_string="$(echo $fixes_list | sed 's/ /~ and /g; s,\([0-9]\+\),`#\1 <https://github.com/coq/coq/issues/\1>`_,g' | tr '~' '\n')" +if [ ! -z "$fixes_string" ]; then fixes_string="$(printf '\n fixes %s,' "$fixes_string")"; fi + # shellcheck disable=SC2016 # the ` are regular strings, this is intended # use %s for the leading - to avoid looking like an option (not sure # if necessary but doesn't hurt) -printf '%s **%s:**\n Bla bla\n (`#%s <https://github.com/coq/coq/pull/%s>`_,\n by %s).' - "$type_full" "$PR" "$PR" "$(git config user.name)" > "$where" +printf '%s **%s:**\n Bla bla\n (`#%s <https://github.com/coq/coq/pull/%s>`_,%s\n by %s).' - "$type_full" "$PR" "$PR" "$fixes_string" "$(git config user.name)" > "$where" printf "Name of created changelog file:\n" printf "$where\n" diff --git a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst deleted file mode 100644 index 57bce7e4f6..0000000000 --- a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - Warn when manual implicit arguments are used in unexpected positions - of a term (e.g. in `Check id (forall {x}, x)`) or when a implicit - argument name is shadowed (e.g. in `Check fun f : forall {x:nat} - {x}, nat => f`) - (`#10202 <https://github.com/coq/coq/pull/10202>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst deleted file mode 100644 index 70c57c718f..0000000000 --- a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Added:** - :cmd:`Arguments` now supports setting - implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`. - (`#11098 <https://github.com/coq/coq/pull/11098>`_, - by Hugo Herbelin, fixes `#4696 - <https://github.com/coq/coq/pull/4696>`_, `#5173 - <https://github.com/coq/coq/pull/5173>`_, `#9098 - <https://github.com/coq/coq/pull/9098>`_). diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst deleted file mode 100644 index 768ef68339..0000000000 --- a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Syntax for non-maximal implicit arguments in definitions and terms using - square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]`` - to be consistent with the command :cmd:`Arguments`. - (`#11235 <https://github.com/coq/coq/pull/11235>`_, - by SimonBoulier). diff --git a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst deleted file mode 100644 index 51818c666b..0000000000 --- a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - :cmd:`Implicit Types` are now taken into account for printing. To inhibit it, - unset the :flag:`Printing Use Implicit Types` flag - (`#11261 <https://github.com/coq/coq/pull/11261>`_, - by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_). diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst deleted file mode 100644 index 66139f76e1..0000000000 --- a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - The warning raised when a trailing implicit is declared to be non-maximally - inserted (with the command :cmd:`Arguments`) has been turned into an error. - This was deprecated since Coq 8.10 - (`#11368 <https://github.com/coq/coq/pull/11368>`_, - by SimonBoulier). diff --git a/doc/changelog/02-specification-language/11579-inductive-params.rst b/doc/changelog/02-specification-language/11579-inductive-params.rst deleted file mode 100644 index 28bc8e9592..0000000000 --- a/doc/changelog/02-specification-language/11579-inductive-params.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Fixed:** - More robust and expressive treatment of implicit inductive - parameters in inductive declarations (`#11579 - <https://github.com/coq/coq/pull/11579>`_, by Maxime Dénès, Gaëtan - Gilbert and Jasper Hugunin; fixes `#7253 - <https://github.com/coq/coq/pull/7253>`_ and `#11585 - <https://github.com/coq/coq/pull/11585>`_) diff --git a/doc/changelog/02-specification-language/11600-uniform-syntax.rst b/doc/changelog/02-specification-language/11600-uniform-syntax.rst deleted file mode 100644 index b95bad2eb8..0000000000 --- a/doc/changelog/02-specification-language/11600-uniform-syntax.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - New syntax :g:`Inductive Acc A R | x : Prop := ...` to specify which - parameters of an inductive are uniform. - See :ref:`parametrized-inductive-types` - (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst b/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst deleted file mode 100644 index d69a94205f..0000000000 --- a/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - New warning on using :cmd:`Fixpoint` or :cmd:`CoFixpoint` for - definitions which are not recursive - (`#12121 <https://github.com/coq/coq/pull/12121>`_, - by Hugo Herbelin) diff --git a/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst b/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst deleted file mode 100644 index e5ec865b15..0000000000 --- a/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Anomaly possibly raised when printing binders with implicit types - (`#12323 <https://github.com/coq/coq/pull/12323>`_, - by Hugo Herbelin; fixes `#12322 <https://github.com/coq/coq/pull/12322>`_). diff --git a/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst new file mode 100644 index 0000000000..8f126c5b6f --- /dev/null +++ b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Case of an anomaly in trying to infer the return clause of an ill-typed :g:`match` + (`#12422 <https://github.com/coq/coq/pull/12422>`_, + fixes `#12418 <https://github.com/coq/coq/pull/12418>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst deleted file mode 100644 index a8d4fc6ed2..0000000000 --- a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Different interpretations in different scopes of the same notation - string can now be associated to different printing formats (`#10832 - <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin, - fixes `#6092 <https://github.com/coq/coq/issues/6092>`_ - and `#7766 <https://github.com/coq/coq/issues/7766>`_). diff --git a/doc/changelog/03-notations/11113-remove-compat.rst b/doc/changelog/03-notations/11113-remove-compat.rst deleted file mode 100644 index 3bcdd3dd6f..0000000000 --- a/doc/changelog/03-notations/11113-remove-compat.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **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/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst deleted file mode 100644 index eeb4c755f6..0000000000 --- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst +++ /dev/null @@ -1,17 +0,0 @@ -- **Fixed:** Parsing and printing consistently handle inheritance of implicit - arguments in notations. With the exception of notations of - the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which - inhibit implicit arguments, all notations binding a partially - applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`, - or :n:`Notation @string := (@@qualid {+ @arg })`, or - :n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident - := (@@qualid {+ @arg })`, inherit the remaining implicit arguments - (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo - Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and - `#11091 <https://github.com/coq/coq/pull/11091>`_). - -- **Changed:** Notation scopes are now always inherited in - notations binding a partially applied constant, including for - notations binding an expression of the form :n:`@@qualid`. The latter was - not the case beforehand - (part of `#11120 <https://github.com/coq/coq/pull/11120>`_). 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 deleted file mode 100644 index f377b53ae2..0000000000 --- a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Changed:** - The printing algorithm now interleaves search for notations and removal of coercions - (`#11172 <https://github.com/coq/coq/pull/11172>`_, by Hugo Herbelin). diff --git a/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst deleted file mode 100644 index 1d94cbf21b..0000000000 --- a/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Notations in onlyprinting mode do not uselessly reserve parsing keywords - (`#11590 <https://github.com/coq/coq/pull/11590>`_, - by Hugo Herbelin, fixes `#9741 <https://github.com/coq/coq/pull/9741>`_). diff --git a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst deleted file mode 100644 index 1d30d16664..0000000000 --- a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Notations declared with the ``where`` clause in the declaration of - inductive types, coinductive types, record fields, fixpoints and - cofixpoints now support the ``only parsing`` modifier - (`#11602 <https://github.com/coq/coq/pull/11602>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/11650-parensNew.rst b/doc/changelog/03-notations/11650-parensNew.rst deleted file mode 100644 index f52a720428..0000000000 --- a/doc/changelog/03-notations/11650-parensNew.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - added the :flag:`Printing Parentheses` flag to print parentheses even when implied by associativity or precedence. - (`#11650 <https://github.com/coq/coq/pull/11650>`_, - by Hugo Herbelin and Abhishek Anand). diff --git a/doc/changelog/03-notations/11848-nicer-decimal-printing.rst b/doc/changelog/03-notations/11848-nicer-decimal-printing.rst deleted file mode 100644 index 1d3a390f36..0000000000 --- a/doc/changelog/03-notations/11848-nicer-decimal-printing.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Nicer printing for decimal constants in R and Q. - 1.5 is now printed 1.5 rather than 15e-1. - (`#11848 <https://github.com/coq/coq/pull/11848>`_, - by Pierre Roux). diff --git a/doc/changelog/03-notations/11948-hexadecimal.rst b/doc/changelog/03-notations/11948-hexadecimal.rst deleted file mode 100644 index e4b76d238c..0000000000 --- a/doc/changelog/03-notations/11948-hexadecimal.rst +++ /dev/null @@ -1,12 +0,0 @@ -- **Added:** - Numeral notations now parse hexadecimal constants such as ``0x2a`` - or ``0xb.2ap-2``. Parsers added for :g:`nat`, :g:`positive`, :g:`Z`, - :g:`N`, :g:`Q`, :g:`R`, primitive integers and primitive floats - (`#11948 <https://github.com/coq/coq/pull/11948>`_, - by Pierre Roux). -- **Deprecated:** - Numeral Notation on ``Decimal.uint``, ``Decimal.int`` and - ``Decimal.decimal`` are replaced respectively by numeral notations - on ``Numeral.uint``, ``Numeral.int`` and ``Numeral.numeral`` - (`#11948 <https://github.com/coq/coq/pull/11948>`_, - by Pierre Roux). diff --git a/doc/changelog/03-notations/11986-float-low-level-printing.rst b/doc/changelog/03-notations/11986-float-low-level-printing.rst index f3d85cadc6..aba74891c6 100644 --- a/doc/changelog/03-notations/11986-float-low-level-printing.rst +++ b/doc/changelog/03-notations/11986-float-low-level-printing.rst @@ -1,5 +1,5 @@ - **Added:** - Add flag ``Printing Float`` to print primitive floats as hexadecimal - instead of decimal values. This is included in ``Set Printing All``. + :flag:`Printing Float` flag to print primitive floats as hexadecimal + instead of decimal values. This is included in the :flag:`Printing All` flag (`#11986 <https://github.com/coq/coq/pull/11986>`_, by Pierre Roux). diff --git a/doc/changelog/03-notations/12163-fix-12159.rst b/doc/changelog/03-notations/12163-fix-12159.rst deleted file mode 100644 index 978ed561dd..0000000000 --- a/doc/changelog/03-notations/12163-fix-12159.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **Fixed:** - Numeral Notations now play better with multiple scopes for the same - inductive type. Previously, when multiple numeral notations were defined - for the same inductive, only the last one was considered for - printing. Now, among the notations that are usable for printing and either - have a scope delimiter or are open, the selection is made according - to the order of open scopes, or according to the last defined - notation if no appropriate scope is open - (`#12163 <https://github.com/coq/coq/pull/12163>`_, - fixes `#12159 <https://github.com/coq/coq/pull/12159>`_, - by Pierre Roux, review by Hugo Herbelin and Jason Gross). diff --git a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst deleted file mode 100644 index e1fcfb78c4..0000000000 --- a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Abbreviations support arguments occurring both in term and binder position - (`#8808 <https://github.com/coq/coq/pull/8808>`_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst deleted file mode 100644 index 32cd9b7135..0000000000 --- a/doc/changelog/04-tactics/10760-more-rapply.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Changed:** - The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles - arbitrary numbers of underscores and takes in a :g:`uconstr`. In - rare cases where users were relying on :tacn:`rapply` inserting - exactly 15 underscores and no more, due to the lemma having a - completely unspecified codomain (and thus allowing for any number of - underscores), the tactic will now instead loop (`#10760 - <https://github.com/coq/coq/pull/10760>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst deleted file mode 100644 index ba4d10590f..0000000000 --- a/doc/changelog/04-tactics/10998-zify-complements.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **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`) - are also added to help users to declare new :tacn:`zify` class instances using - Micromega tactics - (`#10998 <https://github.com/coq/coq/pull/10998>`_, by Kazuhiko Sakaguchi). diff --git a/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst deleted file mode 100644 index d510416990..0000000000 --- a/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** The :g:`auto with zarith` tactic and variations (including :tacn:`intuition`) - may now call the :tacn:`lia` tactic instead of :tacn:`omega` - (when the `Omega` module is loaded); - more goals may be automatically solved, - fewer section variables will be captured spuriously - (`#11018 <https://github.com/coq/coq/pull/11018>`_, - by Vincent Laporte). diff --git a/doc/changelog/04-tactics/11025-nativecompute-timing.rst b/doc/changelog/04-tactics/11025-nativecompute-timing.rst deleted file mode 100644 index cb77457c31..0000000000 --- a/doc/changelog/04-tactics/11025-nativecompute-timing.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **Changed:** The :flag:`NativeCompute Timing` flag causes calls to - :tacn:`native_compute` (as well as kernel calls to the native - compiler) to emit separate timing information about conversion to - native code, compilation, execution, and reification. It replaces - the timing information previously emitted when the `-debug` flag was - set, and allows more fine-grained timing of the native compiler - (`#11025 <https://github.com/coq/coq/pull/11025>`_, by Jason Gross). - Additionally, the timing information now uses real time rather than - user time (Fixes `#11962 - <https://github.com/coq/coq/issues/11962>`_, `#11963 - <https://github.com/coq/coq/pull/11963>`_, by Jason Gross) diff --git a/doc/changelog/04-tactics/11288-omega+depr.rst b/doc/changelog/04-tactics/11288-omega+depr.rst deleted file mode 100644 index 3a2d421967..0000000000 --- a/doc/changelog/04-tactics/11288-omega+depr.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Removed:** - The undocumented ``omega with`` tactic variant has been removed, - using :tacn:`lia` is the recommended replacement, although the old semantics - of ``omega with *`` can also be recovered with ``zify; omega`` - (`#11288 <https://github.com/coq/coq/pull/11288>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst deleted file mode 100644 index 20d48929f2..0000000000 --- a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - :tacn:`zify` now handles :g:`Z.pow_pos` by default. - In Coq 8.11, this was the case only when loading module - :g:`ZifyPow` because this triggered a regression of :tacn:`lia`. - The regression is now fixed, and the module kept only for compatibility - (`#11362 <https://github.com/coq/coq/pull/11362>`_, - fixes `#11191 <https://github.com/coq/coq/issues/11191>`_, - by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11370-zify-elim-let.rst b/doc/changelog/04-tactics/11370-zify-elim-let.rst deleted file mode 100644 index 944dde99b8..0000000000 --- a/doc/changelog/04-tactics/11370-zify-elim-let.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Changed:** - Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml - (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11429-zify-optimisation.rst b/doc/changelog/04-tactics/11429-zify-optimisation.rst deleted file mode 100644 index 25927f9182..0000000000 --- a/doc/changelog/04-tactics/11429-zify-optimisation.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Changed:** - Improve the efficiency of :tacn:`zify` by rewritting the remaining Ltac code in OCaml - (`#11429 <https://github.com/coq/coq/pull/11429>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst deleted file mode 100644 index 52a2b2f0f6..0000000000 --- a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Added:** - :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls - (`#11474 <https://github.com/coq/coq/pull/11474>`_, by Frédéric Besson). - -- **Fixed:** - Efficiency regression of :tacn:`lia` - (`#11474 <https://github.com/coq/coq/pull/11474>`_, - fixes `#11436 <https://github.com/coq/coq/issues/11436>`_, - by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst deleted file mode 100644 index 3dd103b115..0000000000 --- a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Syntax :n:`pose proof (@ident:=@term)` as an - alternative to :n:`pose proof @term as @ident`, following the model of - :n:`pose (@ident:=@term)`. See documentation of :tacn:`pose proof` - (`#11522 <https://github.com/coq/coq/pull/11522>`_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/11760-firstorder-leaf.rst b/doc/changelog/04-tactics/11760-firstorder-leaf.rst deleted file mode 100644 index e6e4b827e5..0000000000 --- a/doc/changelog/04-tactics/11760-firstorder-leaf.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - The default tactic used by :g:`firstorder` is - :g:`auto with core` instead of :g:`auto with *`; - see :ref:`decisionprocedures` for details; - old behavior can be reset by using the `-compat 8.12` command-line flag; - to ease the migration of legacy code, the default solver can be set to `debug auto with *` - with `Set Firstorder Solver debug auto with *` - (`#11760 <https://github.com/coq/coq/pull/11760>`_, - by Vincent Laporte). diff --git a/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst b/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst deleted file mode 100644 index 827d484b28..0000000000 --- a/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** - Deprecated syntax `_eqn` for :tacn:`destruct` and :tacn:`remember`. - Use `eqn:` syntax instead - (`#11877 <https://github.com/coq/coq/pull/11877>`_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/11883-fix-autounfold.rst b/doc/changelog/04-tactics/11883-fix-autounfold.rst deleted file mode 100644 index 83ff177380..0000000000 --- a/doc/changelog/04-tactics/11883-fix-autounfold.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Fixed:** - The behavior of :tacn:`autounfold` no longer depends on the names of terms and modules - (`#11883 <https://github.com/coq/coq/pull/11883>`_, - fixes `#7812 <https://github.com/coq/coq/issues/7812>`_, - by Attila Gáspár). -- **Changed:** - `at` clauses can no longer be used with :tacn:`autounfold`. Since they had no effect, it is safe to remove them - (`#11883 <https://github.com/coq/coq/pull/11883>`_, - by Attila Gáspár). -- **Changed:** - :tacn:`autounfold` no longer fails when the :cmd:`Opaque` command is used on constants in the hint databases - (`#11883 <https://github.com/coq/coq/pull/11883>`_, - by Attila Gáspár). diff --git a/doc/changelog/04-tactics/11976-deprecate-omega.rst b/doc/changelog/04-tactics/11976-deprecate-omega.rst deleted file mode 100644 index 59c9612d17..0000000000 --- a/doc/changelog/04-tactics/11976-deprecate-omega.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Deprecated:** - The :tacn:`omega` tactic is deprecated; - use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead - (`#11976 <https://github.com/coq/coq/pull/11976>`_, - by Vincent Laporte). diff --git a/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst deleted file mode 100644 index f10208e9b2..0000000000 --- a/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Tactics with qualified name of the form ``Coq.Init.Notations`` are - now qualified with prefix ``Coq.Init.Ltac``; users of the -noinit - option should now import Coq.Init.Ltac if they want to use Ltac - (`#12023 <https://github.com/coq/coq/pull/12023>`_, - by Hugo Herbelin; minor source of incompatibilities). diff --git a/doc/changelog/04-tactics/12129-add-with-strategy.rst b/doc/changelog/04-tactics/12129-add-with-strategy.rst deleted file mode 100644 index 68558c0cf4..0000000000 --- a/doc/changelog/04-tactics/12129-add-with-strategy.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - New tactical :tacn:`with_strategy` added which behaves like the - command :cmd:`Strategy`, with effects local to the given tactic - (`#12129 <https://github.com/coq/coq/pull/12129>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst deleted file mode 100644 index 055006d3b4..0000000000 --- a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is - indirectly dependent in the goal; the incompatibility can generally - be fixed by first clearing the hypotheses causing an indirect - dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`in *` - instead; similarly, :tacn:`subst` has no more effect on such variables - (`#12146 <https://github.com/coq/coq/pull/12146>`_, - by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_; - fixes `#12139 <https://github.com/coq/coq/pull/12139>`_). diff --git a/doc/changelog/04-tactics/12213-zify-Nat.rst b/doc/changelog/04-tactics/12213-zify-Nat.rst deleted file mode 100644 index 8b744cd193..0000000000 --- a/doc/changelog/04-tactics/12213-zify-Nat.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Added:** - The :tacn:`zify` tactic is now aware of `Nat.le`, `Nat.lt` and `Nat.eq` - (`#12213 <https://github.com/coq/coq/pull/12213>`_, by Frédéric Besson; fixes `#12210 <https://github.com/coq/coq/issues/12210>`_). diff --git a/doc/changelog/04-tactics/12256-unfold-dyn-check.rst b/doc/changelog/04-tactics/12256-unfold-dyn-check.rst deleted file mode 100644 index c2f7065f4c..0000000000 --- a/doc/changelog/04-tactics/12256-unfold-dyn-check.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - The check that unfold arguments were indeed unfoldable has been moved to runtime - (`#12256 <https://github.com/coq/coq/pull/12256>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst b/doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst deleted file mode 100644 index 2402321fad..0000000000 --- a/doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Fixed:** - Wrong type error in tactic :tacn:`functional induction`. - (`#12326 <https://github.com/coq/coq/pull/12326>`_, - by Pierre Courtieu, - fixes `#11761 <https://github.com/coq/coq/issues/11761>`_, - reported by Lasse Blaauwbroek). -- **Changed** - When the tactic :tacn:`functional induction` :n:`c__1 c__2 ... c__n` is used - with no parenthesis around :n:`c__1 c__2 ... c__n`, :n:`c__1 c__2 ... c__n` is now - read as one sinlge applicative term. In particular implicit - arguments should be omitted. Rare source of incompatibility - (`#12326 <https://github.com/coq/coq/pull/12326>`_, - by Pierre Courtieu). diff --git a/doc/changelog/04-tactics/12366-fix-exists.rst b/doc/changelog/04-tactics/12366-fix-exists.rst deleted file mode 100644 index 6d976ff562..0000000000 --- a/doc/changelog/04-tactics/12366-fix-exists.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - When using :tacn:`exists` or :tacn:`eexists` with multiple arguments, - the evaluation of arguments and applications of constructors are now interleaved. - This improves unification in some cases - (`#12366 <https://github.com/coq/coq/pull/12366>`_, - fixes `#12365 <https://github.com/coq/coq/issues/12365>`_, - by Attila Gáspár). diff --git a/doc/changelog/04-tactics/12399-rm-prolog.rst b/doc/changelog/04-tactics/12399-rm-prolog.rst new file mode 100644 index 0000000000..afde7db370 --- /dev/null +++ b/doc/changelog/04-tactics/12399-rm-prolog.rst @@ -0,0 +1,4 @@ +- **Removed:** + The deprecated and undocumented "prolog" tactic was removed + (`#12399 <https://github.com/coq/coq/pull/12399>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst b/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst deleted file mode 100644 index e8233b9d13..0000000000 --- a/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - An array library for Ltac2 (as compatible as possible with OCaml standard library) - (`#10343 <https://github.com/coq/coq/pull/10343>`_, - by Michael Soegtrop). diff --git a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst deleted file mode 100644 index 0dd0fed4e2..0000000000 --- a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to - give a name to the old value so as to be able to reuse it inside the - new one - (`#11503 <https://github.com/coq/coq/pull/11503>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/05-tactic-language/11740-ltac2-enough.rst b/doc/changelog/05-tactic-language/11740-ltac2-enough.rst deleted file mode 100644 index 5d3671bce1..0000000000 --- a/doc/changelog/05-tactic-language/11740-ltac2-enough.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Ltac2 notations for :tacn:`enough` and :tacn:`eenough` - (`#11740 <https://github.com/coq/coq/pull/11740>`_, - by Michael Soegtrop). diff --git a/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst b/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst deleted file mode 100644 index 47e7be4d0e..0000000000 --- a/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - New Ltac2 function ``Fresh.Free.of_goal`` to return the list of - names of declarations of the current goal; new Ltac2 function - ``Fresh.in_goal`` to return a variable fresh in the current goal - (`#11882 <https://github.com/coq/coq/pull/11882>`_, - by Hugo Herbelin). diff --git a/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst b/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst deleted file mode 100644 index 2f8d92fae5..0000000000 --- a/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Ltac2 notations for reductions in terms: :n:`eval @red_expr in @ltac2_term` - (`#11981 <https://github.com/coq/coq/pull/11981>`_, - by Michael Soegtrop). diff --git a/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst b/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst deleted file mode 100644 index b90c8e7a1f..0000000000 --- a/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - The :flag:`Ltac Profiling` machinery now correctly handles - backtracking into multi-success tactics. The call-counts of some - tactics are unfortunately inflated by 1, as some tactics are - implicitly implemented as :g:`tac + fail`, which has two - entry-points rather than one (Fixes `#12196 - <https://github.com/coq/coq/issues/12196>`_, `#12197 - <https://github.com/coq/coq/pull/12197>`_, by Jason Gross). diff --git a/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst b/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst deleted file mode 100644 index 69632fd202..0000000000 --- a/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - The "reference" tactic generic argument now accepts arbitrary - variables of the goal context - (`#12254 <https://github.com/coq/coq/pull/12254>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/06-ssreflect/8855-master+more-search-options.rst b/doc/changelog/06-ssreflect/8855-master+more-search-options.rst deleted file mode 100644 index 2fdacfd82a..0000000000 --- a/doc/changelog/06-ssreflect/8855-master+more-search-options.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **Changed:** The :cmd:`Search (ssreflect)` command that used to be - available when loading the `ssreflect` plugin has been moved to a - separate plugin that needs to be loaded separately: `ssrsearch` - (part of `#8855 <https://github.com/coq/coq/pull/8855>`_, fixes - `#12253 <https://github.com/coq/coq/issues/12253>`_, by Théo - Zimmermann). - -- **Deprecated:** :cmd:`Search (ssreflect)` (available through - `Require ssrsearch.`) in favor of the `headconcl:` clause of - :cmd:`Search` (part of `#8855 - <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann). diff --git a/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst b/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst deleted file mode 100644 index b627fdbcc9..0000000000 --- a/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Deprecated:** - Deprecated the declaration of arbitrary terms as hints. Global - references are now preferred - (`#7791 <https://github.com/coq/coq/pull/7791>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst deleted file mode 100644 index b263de017b..0000000000 --- a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - The :cmd:`Print Canonical Projections` command can now take constants and - prints only the unification rules that involve or are synthesized from given - constants (`#10747 <https://github.com/coq/coq/pull/10747>`_, - by Kazuhiko Sakaguchi). diff --git a/doc/changelog/07-commands-and-options/11162-local-cs.rst b/doc/changelog/07-commands-and-options/11162-local-cs.rst deleted file mode 100644 index b89e047153..0000000000 --- a/doc/changelog/07-commands-and-options/11162-local-cs.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical - Structure` declarations (`#11162 - <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst deleted file mode 100644 index 2bdc8052c6..0000000000 --- a/doc/changelog/07-commands-and-options/11164-let-cs.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Added:** A section variable introduced with :cmd:`Let` can be - declared as a :cmd:`Canonical Structure` (`#11164 - <https://github.com/coq/coq/pull/11164>`_, 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 deleted file mode 100644 index 9fc09c4189..0000000000 --- a/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **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/07-commands-and-options/11258-coherence.rst b/doc/changelog/07-commands-and-options/11258-coherence.rst deleted file mode 100644 index f04a120417..0000000000 --- a/doc/changelog/07-commands-and-options/11258-coherence.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Changed:** - The :cmd:`Coercion` command has been improved to check the coherence of the - inheritance graph. It checks whether a circular inheritance path of `C >-> C` - is convertible with the identity function or not, then report it as an - ambiguous path if it is not. The new mechanism does not report ambiguous - paths that are redundant with others. For example, checking the ambiguity of - `[f; g]` and `[f'; g]` is redundant with that of `[f]` and `[f']` thus will - not be reported - (`#11258 <https://github.com/coq/coq/pull/11258>`_, - by Kazuhiko Sakaguchi). diff --git a/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst b/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst deleted file mode 100644 index 7bcbb9a8e3..0000000000 --- a/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Added:** Support for universe bindings and universe contrainsts in - :cmd:`Let` definitions (`#11534 - <https://github.com/coq/coq/pull/11534>`_, by Théo Zimmermann). diff --git a/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst b/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst deleted file mode 100644 index d134aeae8b..0000000000 --- a/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** Deprecated unsound compatibility ``Template Check`` - flag that was introduced in 8.10 to help users gradually move their - template polymorphic inductive type definitions outside sections - (`#11546 <https://github.com/coq/coq/pull/11546>`_, by Pierre-Marie - Pédrot). diff --git a/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst b/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst deleted file mode 100644 index 99f2d22d11..0000000000 --- a/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Removed:** - Recursive OCaml loadpaths are not supported anymore; the command - ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the - preferred one. We have also dropped support for the non-qualified - version of the :cmd:`Add LoadPath` command, that is to say, - the ``Add LoadPath dir`` version; now, - you must always specify a prefix now using ``Add Loadpath dir as Prefix`` - (`#11618 <https://github.com/coq/coq/pull/11618>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst deleted file mode 100644 index 419d683037..0000000000 --- a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Removed:** - Unqualified ``polymorphic``, ``monomorphic``, ``template``, - ``notemplate`` attributes (they were deprecated since Coq 8.10). - Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)` and :attr:`universes(notemplate)` instead - (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). diff --git a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst deleted file mode 100644 index 7b690da68d..0000000000 --- a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **Added:** - New attributes supported when defining an inductive type - :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and - :attr:`private(matching)`, which correspond to legacy attributes - ``Cumulative``, ``NonCumulative``, and the so far undocumented - ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by - Théo Zimmermann). - -- **Changed:** :term:`Legacy attributes <attribute>` can now be passed - in any order (`#11665 <https://github.com/coq/coq/pull/11665>`_, by - Théo Zimmermann). diff --git a/doc/changelog/07-commands-and-options/11746-remove-chapter.rst b/doc/changelog/07-commands-and-options/11746-remove-chapter.rst deleted file mode 100644 index 0316432b0a..0000000000 --- a/doc/changelog/07-commands-and-options/11746-remove-chapter.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Removed:** undocumented ``Chapter`` command. Use :cmd:`Section` - instead (`#11746 <https://github.com/coq/coq/pull/11746>`_, by Théo - Zimmermann). diff --git a/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst b/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst deleted file mode 100644 index 5b0cdb5914..0000000000 --- a/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Several commands (`Search`, `About`, ...) now print the implicit arguments - in brackets when printing types. - (`#11795 <https://github.com/coq/coq/pull/11795>`_, - by SimonBoulier). diff --git a/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst b/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst deleted file mode 100644 index 9341eebb58..0000000000 --- a/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - the :cmd:`Hint` commands now accept the :attr:`export` locality as - an attribute, allowing to make import-scoped hints - (`#11812 <https://github.com/coq/coq/pull/11812>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst b/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst deleted file mode 100644 index 5ab2941446..0000000000 --- a/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Deprecated:** - Option :flag:`Hide Obligations` has been deprecated - (`#11828 <https://github.com/coq/coq/pull/11828>`_, - by Emilio Jesus Gallego Arias). - -- **Removed:** - Deprecated option ``Shrink Obligations`` has been removed - (`#11828 <https://github.com/coq/coq/pull/11828>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst deleted file mode 100644 index e409c638bb..0000000000 --- a/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Removed:** Removed SearchAbout command that was deprecated in 8.5. - Use :cmd:`Search` instead. - (`#11944 <https://github.com/coq/coq/pull/11944>`_, by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/11972-fix-require-in-section.rst b/doc/changelog/07-commands-and-options/11972-fix-require-in-section.rst new file mode 100644 index 0000000000..7e34c4a0ff --- /dev/null +++ b/doc/changelog/07-commands-and-options/11972-fix-require-in-section.rst @@ -0,0 +1,5 @@ +- **Changed:** The warning when using :cmd:`Require` inside a section + moved from the ``deprecated`` category to the ``fragile`` category, + because there is no plan to remove the functionality at this time. + (`#11972 <https://github.com/coq/coq/pull/11972>`_, by Gaëtan + Gilbert). diff --git a/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst deleted file mode 100644 index ad7cf44482..0000000000 --- a/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Added :flag:`Cumulative StrictProp` to control cumulativity of - |SProp| and deprecated now redundant command line - ``--cumulative-sprop`` (`#12034 - <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst b/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst deleted file mode 100644 index 259253ec79..0000000000 --- a/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - A printing bug in the presence of elimination principles with local definitions - (`#12295 <https://github.com/coq/coq/pull/12295>`_, - by Hugo Herbelin; fixes `#12233 <https://github.com/coq/coq/pull/12233>`_). diff --git a/doc/changelog/07-commands-and-options/12296-master+fix12234-show-proof-proper.rst b/doc/changelog/07-commands-and-options/12296-master+fix12234-show-proof-proper.rst deleted file mode 100644 index dc71a27eb8..0000000000 --- a/doc/changelog/07-commands-and-options/12296-master+fix12234-show-proof-proper.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Anomalies with :cmd:`Show Proof` - (`#12296 <https://github.com/coq/coq/pull/12296>`_, - by Hugo Herbelin; fixes - `#12234 <https://github.com/coq/coq/pull/12234>`_). diff --git a/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst deleted file mode 100644 index 5b35090d7e..0000000000 --- a/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - :cmd:Redirect now obeys the :opt:`Printing Width` and - :opt:`Printing Depth` flags. - (`#12358 <https://github.com/coq/coq/pull/12358>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst b/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst deleted file mode 100644 index cd993bf356..0000000000 --- a/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Added:** Support for new clauses `hyp:`, `headhyp:`, `concl:`, - `headconcl:`, `head:` and `is:` in :cmd:`Search`. Support for - complex search queries combining disjunctions, conjunctions and - negations (`#8855 <https://github.com/coq/coq/pull/8855>`_, by Hugo - Herbelin, with ideas from Cyril Cohen and help from Théo - Zimmermann). -- **Deprecated:** :cmd:`SearchHead` in favor of the new `headconcl:` - clause of :cmd:`Search` (part of `#8855 - <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann). diff --git a/doc/changelog/08-tools/10592-coqdoc-details.rst b/doc/changelog/08-tools/10592-coqdoc-details.rst deleted file mode 100644 index c5bdc1dbb0..0000000000 --- a/doc/changelog/08-tools/10592-coqdoc-details.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - A new documentation environment ``details`` to make certain portion - of a Coq document foldable. See :ref:`coqdoc` - (`#10592 <https://github.com/coq/coq/pull/10592>`_, - by Thomas Letan). diff --git a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst deleted file mode 100644 index 3b20bbf75d..0000000000 --- a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst +++ /dev/null @@ -1,35 +0,0 @@ -- **Added:** - The ``make-both-single-timing-files.py`` script now accepts a - ``--fuzz=N`` parameter on the command line which determines how many - characters two lines may be offset in the "before" and "after" - timing logs while still being considered the same line. When - invoking this script via the ``print-pretty-single-time-diff`` - target in a ``Makefile`` made by ``coq_makefile``, you can set this - argument by passing ``TIMING_FUZZ=N`` to ``make`` (`#11302 - <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). - -- **Added:** - The ``make-one-time-file.py`` and ``make-both-time-files.py`` - scripts now accept a ``--real`` parameter on the command line to - print real times rather than user times in the tables. The - ``make-both-single-timing-files.py`` script accepts a ``--user`` - parameter to use user times. When invoking these scripts via the - ``print-pretty-timed`` or ``print-pretty-timed-diff`` or - ``print-pretty-single-time-diff`` targets in a ``Makefile`` made by - ``coq_makefile``, you can set this argument by passing - ``TIMING_REAL=1`` (to pass ``--real``) or ``TIMING_REAL=0`` (to pass - ``--user``) to ``make`` (`#11302 - <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). - -- **Added:** - Coq's build system now supports both ``TIMING_FUZZ``, - ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile`` - made by ``coq_makefile`` (`#11302 - <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). - -- **Fixed:** - The various timing targets for Coq's standard library now correctly - display and label the "before" and "after" columns, rather than - mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_ - fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason - Gross). diff --git a/doc/changelog/08-tools/11409-mltop+deprecate_use.rst b/doc/changelog/08-tools/11409-mltop+deprecate_use.rst deleted file mode 100644 index f4f110ed67..0000000000 --- a/doc/changelog/08-tools/11409-mltop+deprecate_use.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** - The `-load-ml-source` and `-load-ml-object` command line options - have been removed; their use was very limited, you can achieve the same adding - additional object files in the linking step or using a plugin - (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/08-tools/11523-coqdep+refactor2.rst b/doc/changelog/08-tools/11523-coqdep+refactor2.rst deleted file mode 100644 index 3f93d60926..0000000000 --- a/doc/changelog/08-tools/11523-coqdep+refactor2.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Changed:** - Internal options and behavior of ``coqdep`` have changed. ``coqdep`` - no longer works as a replacement for ``ocamldep``, thus ``.ml`` - files are not supported as input. Also, several deprecated options - have been removed: ``-w``, ``-D``, ``-mldep``, ``-prefix``, - ``-slash``, and ``-dumpbox``. Passing ``-boot`` to ``coqdep`` will - not load any path by default now, ``-R/-Q`` should be used instead - (`#11523 <https://github.com/coq/coq/pull/11523>`_ and - `#11589 <https://github.com/coq/coq/pull/11589>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/08-tools/11606-memory-in-timing-scripts.rst b/doc/changelog/08-tools/11606-memory-in-timing-scripts.rst deleted file mode 100644 index e09c6ef3a3..0000000000 --- a/doc/changelog/08-tools/11606-memory-in-timing-scripts.rst +++ /dev/null @@ -1,25 +0,0 @@ -- **Added:** - The ``make-one-time-file.py`` and ``make-both-time-files.py`` - scripts now include peak memory usage information in the tables (can - be turned off by the ``--no-include-mem`` command-line parameter), - and a ``--sort-by-mem`` parameter to sort the tables by memory - rather than time. When invoking these scripts via the - ``print-pretty-timed`` or ``print-pretty-timed-diff`` targets in a - ``Makefile`` made by ``coq_makefile``, you can set this argument by - passing ``TIMING_INCLUDE_MEM=0`` (to pass ``--no-include-mem``) and - ``TIMING_SORT_BY_MEM=1`` (to pass ``--sort-by-mem``) to ``make`` - (`#11606 <https://github.com/coq/coq/pull/11606>`_, by Jason Gross). - -- **Added:** - Coq's build system now supports both ``TIMING_INCLUDE_MEM`` and - ``TIMING_SORT_BY_MEM`` just like a ``Makefile`` made by - ``coq_makefile`` (`#11606 <https://github.com/coq/coq/pull/11606>`_, - by Jason Gross). - -- **Changed:** - The sorting order of the timing script ``make-both-time-files.py`` - and the target ``print-pretty-timed-diff`` is now deterministic even - when the sorting order is ``absolute`` or ``diff``; previously the - relative ordering of two files with identical times was - non-deterministic (`#11606 - <https://github.com/coq/coq/pull/11606>`_, by Jason Gross). diff --git a/doc/changelog/08-tools/11617-toplevel+boot.rst b/doc/changelog/08-tools/11617-toplevel+boot.rst deleted file mode 100644 index 49dd0ee2d8..0000000000 --- a/doc/changelog/08-tools/11617-toplevel+boot.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the - `Coq` library prefix by default - (`#11617 <https://github.com/coq/coq/pull/11617>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst deleted file mode 100644 index ff736641b4..0000000000 --- a/doc/changelog/08-tools/11851-coqc-flags-fix.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - The order in which the require flags `-ri`, `-re`, `-rfrom`, etc. - and the option flags `-set`, `-unset` are given now matters. In - particular, it is now possible to interleave the loading of plugins - and the setting of options by choosing the right order for these - flags. The load flags `-l` and `-lv` are still processed afterward - for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and - `#12097 <https://github.com/coq/coq/pull/12097>`_, - by Lasse Blaauwbroek). diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst deleted file mode 100644 index affb685fcb..0000000000 --- a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** - Confusingly-named and deprecated since 8.11 `-require` option. - Use the equivalent `-require-import` instead - (`#12005 <https://github.com/coq/coq/pull/12005>`_, - by Théo Zimmermann). diff --git a/doc/changelog/08-tools/12006-issue5632.rst b/doc/changelog/08-tools/12006-issue5632.rst deleted file mode 100644 index 162d56b1b6..0000000000 --- a/doc/changelog/08-tools/12006-issue5632.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - ``Makefile`` generated by ``coq_makefile`` erases ``.lia.cache`` and ``.nia.cache`` by ``make cleanall``. - (`#12006 <https://github.com/coq/coq/pull/12006>`_, - by Olivier Laurent). diff --git a/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst deleted file mode 100644 index 5c4ef82b8b..0000000000 --- a/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Definitions in coqdoc link to themselves, giving access in html to their own url - (`#12026 <https://github.com/coq/coq/pull/12026>`_, - by Hugo Herbelin; granting `#7093 <https://github.com/coq/coq/pull/7093>`_). diff --git a/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst b/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst deleted file mode 100644 index ae9b69e592..0000000000 --- a/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Fields of a record tuple now link in coqdoc to their definition - (`#12027 <https://github.com/coq/coq/pull/12027>`_, fixes - `#3415 <https://github.com/coq/coq/issues/3415>`_, - by Hugo Herbelin; ). diff --git a/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst b/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst deleted file mode 100644 index af0d28305a..0000000000 --- a/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Add hyperlinks on bound variables for coqdoc - (`#12033 <https://github.com/coq/coq/pull/12033>`_, - by Hugo Herbelin; it incidentally fixes - `#7697 <https://github.com/coq/coq/pull/7697>`_). diff --git a/doc/changelog/08-tools/12037-coqdoc-preformatted.rst b/doc/changelog/08-tools/12037-coqdoc-preformatted.rst deleted file mode 100644 index bf65719516..0000000000 --- a/doc/changelog/08-tools/12037-coqdoc-preformatted.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - ``coqdoc`` now reports the location of a mismatched opening ``[[`` instead of - throwing an uninformative exception. - (`#12037 <https://github.com/coq/coq/pull/12037>`_, - fixes `#9670 <https://github.com/coq/coq/issues/9670>`_, - by Lysxia). diff --git a/doc/changelog/08-tools/12076-fix-5030.rst b/doc/changelog/08-tools/12076-fix-5030.rst deleted file mode 100644 index afb59b1cde..0000000000 --- a/doc/changelog/08-tools/12076-fix-5030.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Fix #5030 (coqchk reports names from opaque modules as axioms) - (`#12076 <https://github.com/coq/coq/pull/12076>`_, - by Pierre Roux). diff --git a/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst deleted file mode 100644 index f6af5d40e8..0000000000 --- a/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - ``Coqdoc``: Highlighting of the exact position of the target of links - (`#12091 <https://github.com/coq/coq/pull/12091>`_, - by Hugo Herbelin). diff --git a/doc/changelog/08-tools/12126-adjust-timed-name.rst b/doc/changelog/08-tools/12126-adjust-timed-name.rst deleted file mode 100644 index c305b384d9..0000000000 --- a/doc/changelog/08-tools/12126-adjust-timed-name.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Changed:** - The output of ``make TIMED=1`` (and therefore the timing targets - such as ``print-pretty-timed`` and ``print-pretty-timed-diff``) now - displays the full name of the output file being built, rather than - the stem of the rule (which was usually the filename without the - extension, but in general could be anything for user-defined rules - involving ``%``) (`#12126 - <https://github.com/coq/coq/pull/12126>`_, by Jason Gross). diff --git a/doc/changelog/08-tools/12211-time-ocaml.rst b/doc/changelog/08-tools/12211-time-ocaml.rst deleted file mode 100644 index 7ff68cc495..0000000000 --- a/doc/changelog/08-tools/12211-time-ocaml.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - When passing ``TIMED=1`` to ``make`` with either Coq's own makefile - or a ``coq_makefile``\-made makefile, timing information is now - printed for OCaml files as well (`#12211 - <https://github.com/coq/coq/pull/12211>`_, by Jason Gross). diff --git a/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst b/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst deleted file mode 100644 index 8a43f5af94..0000000000 --- a/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - The pretty-timed scripts and targets now print a newline at the end of their - tables, rather than creating text with no trailing newline (`#12368 - <https://github.com/coq/coq/pull/12368>`_, by Jason Gross). diff --git a/doc/changelog/08-tools/12389-coq_makefile.rst b/doc/changelog/08-tools/12389-coq_makefile.rst new file mode 100644 index 0000000000..74e3a68170 --- /dev/null +++ b/doc/changelog/08-tools/12389-coq_makefile.rst @@ -0,0 +1,5 @@ +- **Changed:** + Adding the possibility in coq_makefile to directly set the installation folders, + through the :n:`COQLIBINSTALL` and :n:`COQDOCINSTALL` variables. + See :ref:`coqmakefilelocal`. + (`#12389 <https://github.com/coq/coq/pull/12389>`_, by Martin Bodin, review of Enrico Tassi). diff --git a/doc/changelog/08-tools/12410-add-fixes.rst b/doc/changelog/08-tools/12410-add-fixes.rst new file mode 100644 index 0000000000..f4c41dc3c3 --- /dev/null +++ b/doc/changelog/08-tools/12410-add-fixes.rst @@ -0,0 +1,4 @@ +- **Changed:** + ``dev/tools/make-changelog.sh`` now asks for a list of bugs fixed by the PR + (`#12410 <https://github.com/coq/coq/pull/12410>`_, fixes `#12386 + <https://github.com/coq/coq/issues/12386>`_, by Jason Gross). diff --git a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst deleted file mode 100644 index 49ac16eee9..0000000000 --- a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - "Tactic" menu from CoqIDE which had been unmaintained for a number of years - (`#11414 <https://github.com/coq/coq/pull/11414>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst deleted file mode 100644 index 9d22a858f1..0000000000 --- a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - "Revert all buffers" command from CoqIDE which had been broken for a long time - (`#11415 <https://github.com/coq/coq/pull/11415>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/11127-trunk.rst b/doc/changelog/10-standard-library/11127-trunk.rst deleted file mode 100644 index 3f461397ae..0000000000 --- a/doc/changelog/10-standard-library/11127-trunk.rst +++ /dev/null @@ -1,2 +0,0 @@ -- **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/10-standard-library/11240-rew-dependent.rst b/doc/changelog/10-standard-library/11240-rew-dependent.rst deleted file mode 100644 index e9daab0c2c..0000000000 --- a/doc/changelog/10-standard-library/11240-rew-dependent.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added** - Added :g:`rew dependent` notations for the dependent version of - :g:`rew` in :g:`Coq.Init.Logic.EqNotations` to improve the display - and parsing of :g:`match` statements on :g:`Logic.eq` (`#11240 - <https://github.com/coq/coq/pull/11240>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst b/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst deleted file mode 100644 index be54e45808..0000000000 --- a/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst +++ /dev/null @@ -1,18 +0,0 @@ -- **Added:** - lemmas about lists: - - - properties of ``In``: ``in_elt``, ``in_elt_inv`` - - properties of ``nth``: ``app_nth2_plus``, ``nth_middle``, ``nth_ext`` - - properties of ``last``: ``last_last``, ``removelast_last`` - - properties of ``remove``: ``remove_cons``, ``remove_app``, ``notin_remove``, ``in_remove``, ``in_in_remove``, ``remove_remove_comm``, ``remove_remove_eq``, ``remove_length_le``, ``remove_length_lt`` - - properties of ``concat``: ``in_concat``, ``remove_concat`` - - properties of ``map`` and ``flat_map``: ``map_last``, ``map_eq_cons``, ``map_eq_app``, ``flat_map_app``, ``flat_map_ext``, ``nth_nth_nth_map`` - - properties of ``incl``: ``incl_nil_l``, ``incl_l_nil``, ``incl_cons_inv``, ``incl_app_app``, ``incl_app_inv``, ``remove_incl``, ``incl_map``, ``incl_filter``, ``incl_Forall_in_iff`` - - properties of ``NoDup`` and ``nodup``: ``NoDup_rev``, ``NoDup_filter``, ``nodup_incl`` - - properties of ``Exists`` and ``Forall``: ``Exists_nth``, ``Exists_app``, ``Exists_rev``, ``Exists_fold_right``, ``incl_Exists``, ``Forall_nth``, ``Forall_app``, ``Forall_elt``, ``Forall_rev``, ``Forall_fold_right``, ``incl_Forall``, ``map_ext_Forall``, ``Exists_or``, ``Exists_or_inv``, ``Forall_and``, ``Forall_and_inv``, ``exists_Forall``, ``Forall_image``, ``concat_nil_Forall``, ``in_flat_map_Exists``, ``notin_flat_map_Forall`` - - properties of ``repeat``: ``repeat_cons``, ``repeat_to_concat`` - - definitions and properties of ``list_sum`` and ``list_max``: ``list_sum_app``, ``list_max_app``, ``list_max_le``, ``list_max_lt`` - - misc: ``elt_eq_unit``, ``last_length``, ``rev_eq_app``, ``removelast_firstn_len``, ``cons_seq``, ``seq_S`` - - (`#11249 <https://github.com/coq/coq/pull/11249>`_, `#12237 <https://github.com/coq/coq/pull/12237>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/11335-ollibs-wfnat-changelog.rst b/doc/changelog/10-standard-library/11335-ollibs-wfnat-changelog.rst deleted file mode 100644 index 0eb3eefde5..0000000000 --- a/doc/changelog/10-standard-library/11335-ollibs-wfnat-changelog.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Well-founded induction principles for `nat`: ``lt_wf_rect1``, ``lt_wf_rect``, ``gt_wf_rect``, ``lt_wf_double_rect`` - (`#11335 <https://github.com/coq/coq/pull/11335>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/11350-list.rst b/doc/changelog/10-standard-library/11350-list.rst deleted file mode 100644 index 52c2517161..0000000000 --- a/doc/changelog/10-standard-library/11350-list.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - ``remove'`` and ``count_occ'`` over lists, - alternatives to ``remove`` and ``count_occ`` based on ``filter`` - (`#11350 <https://github.com/coq/coq/pull/11350>`_, - by Yishuai Li). diff --git a/doc/changelog/10-standard-library/11404-removeRList.rst b/doc/changelog/10-standard-library/11404-removeRList.rst deleted file mode 100644 index 88e22d128c..0000000000 --- a/doc/changelog/10-standard-library/11404-removeRList.rst +++ /dev/null @@ -1,15 +0,0 @@ -- **Removed:** - Type `RList` has been removed. All uses have been replaced by `list R`. - Functions from `RList` named `In`, `Rlength`, `cons_Rlist`, `app_Rlist` - have also been removed as they are essentially the same as `In`, `length`, - `app`, and `map` from `List`, modulo the following changes: - - - `RList.In x (RList.cons a l)` used to be convertible to - `(x = a) \\/ RList.In x l`, - but `List.In x (a :: l)` is convertible to - `(a = x) \\/ List.In l`. - The equality is reversed. - - `app_Rlist` and `List.map` take arguments in different order. - - (`#11404 <https://github.com/coq/coq/pull/11404>`_, - by Yves Bertot). diff --git a/doc/changelog/10-standard-library/11686-fix-int-notations.rst b/doc/changelog/10-standard-library/11686-fix-int-notations.rst deleted file mode 100644 index 4959a9f9b1..0000000000 --- a/doc/changelog/10-standard-library/11686-fix-int-notations.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Notations :n:`[|@term|]` and :n:`[||@term||]` for morphisms from 63-bit - integers to :g:`Z` and :g:`zn2z int` have been removed in favor of - :n:`φ(@term)` and :n:`Φ(@term)` respectively. These notations were - breaking Ltac parsing (`#11686 <https://github.com/coq/coq/pull/11686>`_, - by Maxime Dénès). diff --git a/doc/changelog/10-standard-library/11725-cleanup-reals.rst b/doc/changelog/10-standard-library/11725-cleanup-reals.rst deleted file mode 100644 index 02ee7e6c70..0000000000 --- a/doc/changelog/10-standard-library/11725-cleanup-reals.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Use implicit arguments for ``ConstructiveReals``. Move ``ConstructiveReals`` - into new directory ``Abstract``. Remove imports of implementations inside - those ``Abstract`` files. Move implementation by means of Cauchy sequences in new directory ``Cauchy``. - (`#11725 <https://github.com/coq/coq/pull/11725>`_, - by Vincent Semeria). diff --git a/doc/changelog/10-standard-library/1185-sort.rst b/doc/changelog/10-standard-library/1185-sort.rst deleted file mode 100644 index edb5ee3ac4..0000000000 --- a/doc/changelog/10-standard-library/1185-sort.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - The names of ``Sorted_sort`` and ``LocallySorted_sort`` in ``Coq.Sorting.MergeSort`` - have been swapped to appropriately reflect their meanings - (`#1185 <https://github.com/coq/coq/pull/1185>`_, - by Lysxia). diff --git a/doc/changelog/10-standard-library/11880-iter.rst b/doc/changelog/10-standard-library/11880-iter.rst deleted file mode 100644 index be4e44ce4c..0000000000 --- a/doc/changelog/10-standard-library/11880-iter.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Added:** - Facts about ``N.iter`` and ``Pos.iter``: - - - ``N.iter_swap_gen``, ``N.iter_swap``, ``N.iter_succ``, ``N.iter_succ_r``, ``N.iter_add``, ``N.iter_ind``, ``N.iter_invariant``; - - ``Pos.iter_succ_r``, ``Pos.iter_ind``. - - (`#11880 <https://github.com/coq/coq/pull/11880>`_, - by Lysxia). diff --git a/doc/changelog/10-standard-library/11891-fix-order-notations.rst b/doc/changelog/10-standard-library/11891-fix-order-notations.rst deleted file mode 100644 index d58d26244a..0000000000 --- a/doc/changelog/10-standard-library/11891-fix-order-notations.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Changed:** - Notations :g:`<=?` and :g:`<?` from ``Coq.Structures.Orders`` and - ``Coq.Sorting.Mergesort.NatOrder`` are now at level 70 rather than - 35, so as to be compatible with the notations defined everywhere - else in the standard library. This may require re-parenthesizing - some expressions. These notations were breaking the ability to - import modules from the standard library that were otherwise - compatible (fixes `#11890 - <https://github.com/coq/coq/issues/11890>`_, `#11891 - <https://github.com/coq/coq/pull/11891>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/11909-fix-≡-level.rst b/doc/changelog/10-standard-library/11909-fix-≡-level.rst deleted file mode 100644 index 96551be537..0000000000 --- a/doc/changelog/10-standard-library/11909-fix-≡-level.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - The level of :g:`≡` in ``Coq.Numbers.Cyclic.Int63.Int63`` is now 70, - no associativity, in line with :g:`=`. Note that this is a minor - incompatibility with developments that declare their own :g:`≡` - notation and import ``Int63`` (fixes `#11905 - <https://github.com/coq/coq/issues/11905>`_, `#11909 - <https://github.com/coq/coq/pull/11909>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/11946-ollibs-permutation.rst b/doc/changelog/10-standard-library/11946-ollibs-permutation.rst deleted file mode 100644 index 626677d31a..0000000000 --- a/doc/changelog/10-standard-library/11946-ollibs-permutation.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Added:** - Facts about ``Permutation``: - - - structure: ``Permutation_refl'``, ``Permutation_morph_transp`` - - compatibilities: ``Permutation_app_rot``, ``Permutation_app_swap_app``, ``Permutation_app_middle``, ``Permutation_middle2``, ``Permutation_elt``, ``Permutation_Forall``, ``Permutation_Exists``, ``Permutation_Forall2``, ``Permutation_flat_map``, ``Permutation_list_sum``, ``Permutation_list_max`` - - inversions: ``Permutation_app_inv_m``, ``Permutation_vs_elt_inv``, ``Permutation_vs_cons_inv``, ``Permutation_vs_cons_cons_inv``, ``Permutation_map_inv``, ``Permutation_image``, ``Permutation_elt_map_inv`` - - length-preserving definition by means of transpositions ``Permutation_transp`` with associated properties: ``Permutation_transp_sym``, ``Permutation_transp_equiv``, ``Permutation_transp_cons``, ``Permutation_Permutation_transp``, ``Permutation_ind_transp`` - - (`#11946 <https://github.com/coq/coq/pull/11946>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/11957-signotations.rst b/doc/changelog/10-standard-library/11957-signotations.rst deleted file mode 100644 index fc5d434274..0000000000 --- a/doc/changelog/10-standard-library/11957-signotations.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - notations for sigma types: ``{ x & P & Q }``, ``{ ' pat & P }``, ``{ ' pat & P & Q }`` - (`#11957 <https://github.com/coq/coq/pull/11957>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/11992-no-reexports.rst b/doc/changelog/10-standard-library/11992-no-reexports.rst deleted file mode 100644 index 3f46bfd501..0000000000 --- a/doc/changelog/10-standard-library/11992-no-reexports.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - No longer re-export ``ListNotations`` from ``Program`` (``Program.Syntax``) - (`#11992 <https://github.com/coq/coq/pull/11992>`_, - by Antonio Nikishaev). diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst deleted file mode 100644 index 42e5eb96eb..0000000000 --- a/doc/changelog/10-standard-library/12008-ollibs-bool.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Order relations ``lt`` and ``compare`` added in ``Bool.Bool``. - Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx`` - (`#12008 <https://github.com/coq/coq/pull/12008>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12014-ollibs-vector.rst b/doc/changelog/10-standard-library/12014-ollibs-vector.rst deleted file mode 100644 index 87625dd23b..0000000000 --- a/doc/changelog/10-standard-library/12014-ollibs-vector.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Added:** - Properties of some operations on vectors: - - - ``nth_order``: ``nth_order_hd``, ``nth_order_tl``, ``nth_order_ext`` - - ``replace``: ``nth_order_replace_eq``, ``nth_order_replace_neq``, ``replace_id``, ``replace_replace_eq``, ``replace_replace_neq`` - - ``map``: ``map_id``, ``map_map``, ``map_ext_in``, ``map_ext`` - - ``Forall`` and ``Forall2``: ``Forall_impl``, ``Forall_forall``, ``Forall_nth_order``, ``Forall2_nth_order`` - - (`#12014 <https://github.com/coq/coq/pull/12014>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12018-master+implb-characterization.rst b/doc/changelog/10-standard-library/12018-master+implb-characterization.rst deleted file mode 100644 index 4b0abdfa3b..0000000000 --- a/doc/changelog/10-standard-library/12018-master+implb-characterization.rst +++ /dev/null @@ -1,19 +0,0 @@ -- **Added:** - Added lemmas - :g:`orb_negb_l`, - :g:`andb_negb_l`, - :g:`implb_true_iff`, - :g:`implb_false_iff`, - :g:`implb_true_r`, - :g:`implb_false_r`, - :g:`implb_true_l`, - :g:`implb_false_l`, - :g:`implb_same`, - :g:`implb_contrapositive`, - :g:`implb_negb`, - :g:`implb_curry`, - :g:`implb_andb_distrib_r`, - :g:`implb_orb_distrib_r`, - :g:`implb_orb_distrib_l` in library :g:`Bool` - (`#12018 <https://github.com/coq/coq/pull/12018>`_,` - by Hugo Herbelin).` diff --git a/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst b/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst deleted file mode 100644 index 95b4cce2f7..0000000000 --- a/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Definition and properties of cyclic permutations / circular shifts: ``CPermutation`` - (`#12031 <https://github.com/coq/coq/pull/12031>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12044-issue-12015.rst b/doc/changelog/10-standard-library/12044-issue-12015.rst deleted file mode 100644 index 166fc80fb0..0000000000 --- a/doc/changelog/10-standard-library/12044-issue-12015.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Fixed:** - Rewrote ``Structures.OrderedTypeEx.String_as_OT.compare`` - to avoid huge proof terms - (Fixes `#12015 <https://github.com/coq/coq/issues/12015>`_, - `#12044 <https://github.com/coq/coq/pull/12044>`_, - by formalize.eth (formalize@protonmail.com)). -- **Added:** - Added ``Structures.OrderedTypeEx.Ascii_as_OT`` - (`#12044 <https://github.com/coq/coq/pull/12044>`_, - by formalize.eth (formalize@protonmail.com)). diff --git a/doc/changelog/10-standard-library/12073-split-nsatz.rst b/doc/changelog/10-standard-library/12073-split-nsatz.rst deleted file mode 100644 index bc3c24e441..0000000000 --- a/doc/changelog/10-standard-library/12073-split-nsatz.rst +++ /dev/null @@ -1,11 +0,0 @@ -- **Changed:** - It is now possible to import the :g:`nsatz` machinery without - transitively depending on the axioms of the real numbers nor of - classical logic by loading ``Coq.nsatz.NsatzTactic`` rather than - ``Coq.nsatz.Nsatz``. Note that some constants have changed kernel - names, living in ``Coq.nsatz.NsatzTactic`` rather than - ``Coq.nsatz.Nsatz``; this might cause minor incompatibilities that - can be fixed by actually running :g:`Import Nsatz` rather than - relying on absolute names (fixes `#5445 - <https://github.com/coq/coq/issues/5445>`_, `#12073 - <https://github.com/coq/coq/pull/12073>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12119-issue12119.rst b/doc/changelog/10-standard-library/12119-issue12119.rst deleted file mode 100644 index 42672b1465..0000000000 --- a/doc/changelog/10-standard-library/12119-issue12119.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - new lemma ``NoDup_incl_NoDup`` in ``List.v`` - to remove useless hypothesis `NoDup l'` in ``Sorting.Permutation.NoDup_Permutation_bis`` - (`#12119 <https://github.com/coq/coq/pull/12119>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst b/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst deleted file mode 100644 index f22fff0736..0000000000 --- a/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - :cmd:`Fixpoint`\s of the standard library without a recursive call turned - into ordinary :cmd:`Definition`\s - (`#12121 <https://github.com/coq/coq/pull/12121>`_, - by Hugo Herbelin; fixes `#11903 <https://github.com/coq/coq/pull/11903>`_). diff --git a/doc/changelog/10-standard-library/12162-bool-leb.rst b/doc/changelog/10-standard-library/12162-bool-leb.rst deleted file mode 100644 index 6a4070a82e..0000000000 --- a/doc/changelog/10-standard-library/12162-bool-leb.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le`` is made local to avoid conflicts with ``Nat.le``. As a consequence, previous calls to ``leb`` based on importing ``Bool`` should now be qualified into ``Bool.le`` even if ``Bool`` is imported. - (`#12162 <https://github.com/coq/coq/pull/12162>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst b/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst deleted file mode 100644 index c80a070181..0000000000 --- a/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Fixed:** - In Haskell extraction with ``ExtrHaskellString``, equality comparisons on - strings and characters are now guaranteed to be uniquely well-typed, even in - very polymorphic contexts under ``unsafeCoerce``; this is achieved by adding - type annotations to the extracted code, and by making ``ExtrHaskellString`` - export ``ExtrHaskellBasic`` (`#12263 - <https://github.com/coq/coq/pull/12263>`_, fixes `#12257 - <https://github.com/coq/coq/issues/12257>`_ and `#12258 - <https://github.com/coq/coq/issues/12258>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12287-zero-of-Q.rst b/doc/changelog/10-standard-library/12287-zero-of-Q.rst deleted file mode 100644 index ba2c74379b..0000000000 --- a/doc/changelog/10-standard-library/12287-zero-of-Q.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - Replace `CRzero` and `CRone` by `CR_of_Q 0` and `CR_of_Q 1` in `ConstructiveReals` - (`#12287 <https://github.com/coq/coq/pull/12287>`_, - by Vincent Semeria). diff --git a/doc/changelog/10-standard-library/12288-constructive-experimental.rst b/doc/changelog/10-standard-library/12288-constructive-experimental.rst deleted file mode 100644 index ec9b66bd7a..0000000000 --- a/doc/changelog/10-standard-library/12288-constructive-experimental.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - Split files `ConstructiveMinMax` and `ConstructivePower`. - - .. warning:: The constructive reals modules are marked as experimental. - - (`#12288 <https://github.com/coq/coq/pull/12288>`_, - by Vincent Semeria). diff --git a/doc/changelog/10-standard-library/9803-reals.rst b/doc/changelog/10-standard-library/9803-reals.rst deleted file mode 100644 index 86c5e45bc1..0000000000 --- a/doc/changelog/10-standard-library/9803-reals.rst +++ /dev/null @@ -1,14 +0,0 @@ -- **Changed:** - Cleanup of names in the Reals theory: replaced `tan_is_inj` with `tan_inj` and replaced `atan_right_inv` with `tan_atan` - - compatibility notations are provided. Moved various auxiliary lemmas from `Ratan.v` to more appropriate places. - (`#9803 <https://github.com/coq/coq/pull/9803>`_, - by Laurent Théry and Michael Soegtrop). - -- **Added:** to the Reals theory: - inverse trigonometric functions `asin` and `acos` with lemmas for the derivatives, bounds and special values of these functions; - an extensive set of identities between trigonometric functions and their inverse functions; - lemmas for the injectivity of sine and cosine; - lemmas on the derivative of the inverse of decreasing functions and on the derivative of horizontally mirrored functions; - various generic auxiliary lemmas and definitions for Rsqr, sqrt, posreal an others. - (`#9803 <https://github.com/coq/coq/pull/9803>`_, - by Laurent Théry and Michael Soegtrop). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst b/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst deleted file mode 100644 index dc76178e0d..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - Python 2 is not longer required in any part of the codebase - (`#11245 <https://github.com/coq/coq/pull/11245>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst b/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst deleted file mode 100644 index 35a618ea8d..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Minimal versions of dependencies for building the reference manual: - now requires Sphinx 2.3.1+, sphinx_rtd_theme 0.4.3+ and - sphinxcontrib-bibtex 0.4.2+ - (`#12224 <https://github.com/coq/coq/pull/12224>`_, - by Jim Fehrle and Théo Zimmermann). diff --git a/doc/changelog/12-misc/10486-native-string-extraction.rst b/doc/changelog/12-misc/10486-native-string-extraction.rst deleted file mode 100644 index 0636e303c4..0000000000 --- a/doc/changelog/12-misc/10486-native-string-extraction.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - Support for better extraction of strings in OCaml and Haskell: - `ExtOcamlNativeString` provides bindings from the Coq `String` type to - the OCaml `string` type, and string literals can be extracted to literals, - both in OCaml and Haskell (`#10486 - <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from - Maxime Dénès, review by Hugo Herbelin). diff --git a/doc/changelog/12-misc/11755-exn+tclfail.rst b/doc/changelog/12-misc/11755-exn+tclfail.rst deleted file mode 100644 index 800cc09e01..0000000000 --- a/doc/changelog/12-misc/11755-exn+tclfail.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Backtrace information for tactics has been improved - (`#11755 <https://github.com/coq/coq/pull/11755>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 363148e2a0..72f0fdf4c5 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -8,6 +8,977 @@ Recent changes .. include:: ../unreleased.rst +Version 8.12 +------------ + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +Changes in 8.12+beta1 +~~~~~~~~~~~~~~~~~~~~~ + +.. contents:: + :local: + +Specification language, type inference +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + The deprecation warning raised since Coq 8.10 when a trailing + implicit is declared to be non-maximally inserted (with the command + :cmd:`Arguments`) has been turned into an error + (`#11368 <https://github.com/coq/coq/pull/11368>`_, + by SimonBoulier). +- **Added:** + Warn when manual implicit arguments are used in unexpected positions + of a term (e.g. in `Check id (forall {x}, x)`) or when an implicit + argument name is shadowed (e.g. in `Check fun f : forall {x:nat} + {x}, nat => f`) + (`#10202 <https://github.com/coq/coq/pull/10202>`_, + by Hugo Herbelin). +- **Added:** + :cmd:`Arguments` now supports setting + implicit an anonymous argument, as e.g. in `Arguments id {A} {_}` + (`#11098 <https://github.com/coq/coq/pull/11098>`_, + by Hugo Herbelin, fixes `#4696 + <https://github.com/coq/coq/pull/4696>`_, `#5173 + <https://github.com/coq/coq/pull/5173>`_, `#9098 + <https://github.com/coq/coq/pull/9098>`_). +- **Added:** + Syntax for non-maximal implicit arguments in definitions and terms using + square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]`` + to be consistent with the command :cmd:`Arguments` + (`#11235 <https://github.com/coq/coq/pull/11235>`_, + by SimonBoulier). +- **Added:** + :cmd:`Implicit Types` are now taken into account for printing. To inhibit it, + unset the :flag:`Printing Use Implicit Types` flag + (`#11261 <https://github.com/coq/coq/pull/11261>`_, + by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_). +- **Added:** + New syntax :cmd:`Inductive` :n:`@ident {* @binder } | {* @binder } := ...` + to specify which parameters of an inductive type are uniform. + See :ref:`parametrized-inductive-types` + (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert). +- **Added:** + Warn when using :cmd:`Fixpoint` or :cmd:`CoFixpoint` for + definitions which are not recursive + (`#12121 <https://github.com/coq/coq/pull/12121>`_, + by Hugo Herbelin). +- **Fixed:** + More robust and expressive treatment of implicit inductive + parameters in inductive declarations (`#11579 + <https://github.com/coq/coq/pull/11579>`_, by Maxime Dénès, Gaëtan + Gilbert and Jasper Hugunin; fixes `#7253 + <https://github.com/coq/coq/pull/7253>`_ and `#11585 + <https://github.com/coq/coq/pull/11585>`_). +- **Fixed:** + Anomaly which could be raised when printing binders with implicit types + (`#12323 <https://github.com/coq/coq/pull/12323>`_, + by Hugo Herbelin; fixes `#12322 <https://github.com/coq/coq/pull/12322>`_). + +Notations +^^^^^^^^^ + +- **Changed:** Notation scopes are now always inherited in + notations binding a partially applied constant, including for + notations binding an expression of the form :n:`@@qualid`. The latter was + not the case beforehand + (part of `#11120 <https://github.com/coq/coq/pull/11120>`_). +- **Changed:** + The printing algorithm now interleaves search for notations and removal of coercions + (`#11172 <https://github.com/coq/coq/pull/11172>`_, by Hugo Herbelin). +- **Changed:** + Nicer printing for decimal constants in R and Q. + 1.5 is now printed 1.5 rather than 15e-1 + (`#11848 <https://github.com/coq/coq/pull/11848>`_, + by Pierre Roux). +- **Removed:** deprecated ``compat`` modifier of :cmd:`Notation` + and :cmd:`Infix` commands. Use the :attr:`deprecated` attribute instead + (`#11113 <https://github.com/coq/coq/pull/11113>`_, + by Théo Zimmermann, with help from Jason Gross). +- **Deprecated:** + Numeral Notation on ``Decimal.uint``, ``Decimal.int`` and + ``Decimal.decimal`` are replaced respectively by numeral notations + on ``Numeral.uint``, ``Numeral.int`` and ``Numeral.numeral`` + (`#11948 <https://github.com/coq/coq/pull/11948>`_, + by Pierre Roux). +- **Added:** + Notations declared with the ``where`` clause in the declaration of + inductive types, coinductive types, record fields, fixpoints and + cofixpoints now support the ``only parsing`` modifier + (`#11602 <https://github.com/coq/coq/pull/11602>`_, + by Hugo Herbelin). +- **Added:** + :flag:`Printing Parentheses` flag to print parentheses even when + implied by associativity or precedence + (`#11650 <https://github.com/coq/coq/pull/11650>`_, + by Hugo Herbelin and Abhishek Anand). +- **Added:** + Numeral notations now parse hexadecimal constants such as ``0x2a`` + or ``0xb.2ap-2``. Parsers added for :g:`nat`, :g:`positive`, :g:`Z`, + :g:`N`, :g:`Q`, :g:`R`, primitive integers and primitive floats + (`#11948 <https://github.com/coq/coq/pull/11948>`_, + by Pierre Roux). +- **Added:** + Abbreviations support arguments occurring both in term and binder position + (`#8808 <https://github.com/coq/coq/pull/8808>`_, + by Hugo Herbelin). +- **Fixed:** + Different interpretations in different scopes of the same notation + string can now be associated to different printing formats (`#10832 + <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin, + fixes `#6092 <https://github.com/coq/coq/issues/6092>`_ + and `#7766 <https://github.com/coq/coq/issues/7766>`_). +- **Fixed:** Parsing and printing consistently handle inheritance of implicit + arguments in notations. With the exception of notations of + the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which + inhibit implicit arguments, all notations binding a partially + applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`, + or :n:`Notation @string := (@@qualid {+ @arg })`, or + :n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident + := (@@qualid {+ @arg })`, inherit the remaining implicit arguments + (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo + Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and + `#11091 <https://github.com/coq/coq/pull/11091>`_). +- **Fixed:** + Notations in ``only printing`` mode do not uselessly reserve parsing keywords + (`#11590 <https://github.com/coq/coq/pull/11590>`_, + by Hugo Herbelin, fixes `#9741 <https://github.com/coq/coq/pull/9741>`_). +- **Fixed:** + Numeral Notations now play better with multiple scopes for the same + inductive type. Previously, when multiple numeral notations were defined + for the same inductive, only the last one was considered for + printing. Now, among the notations that are usable for printing and either + have a scope delimiter or are open, the selection is made according + to the order of open scopes, or according to the last defined + notation if no appropriate scope is open + (`#12163 <https://github.com/coq/coq/pull/12163>`_, + fixes `#12159 <https://github.com/coq/coq/pull/12159>`_, + by Pierre Roux, review by Hugo Herbelin and Jason Gross). + +Tactics +^^^^^^^ + +- **Changed:** + The :tacn:`rapply` tactic in :g:`Coq.Program.Tactics` now handles + arbitrary numbers of underscores and takes in a :g:`uconstr`. In + rare cases where users were relying on :tacn:`rapply` inserting + exactly 15 underscores and no more, due to the lemma having a + completely unspecified codomain (and thus allowing for any number of + underscores), the tactic will now loop instead (`#10760 + <https://github.com/coq/coq/pull/10760>`_, by Jason Gross). +- **Changed:** + The :g:`auto with zarith` tactic and variations (including + :tacn:`intuition`) may now call :tacn:`lia` instead of :tacn:`omega` + (when the `Omega` module is loaded); more goals may be automatically + solved, fewer section variables will be captured spuriously + (`#11018 <https://github.com/coq/coq/pull/11018>`_, + by Vincent Laporte). +- **Changed:** + The new :flag:`NativeCompute Timing` flag causes calls to + :tacn:`native_compute` (as well as kernel calls to the native + compiler) to emit separate timing information about conversion to + native code, compilation, execution, and reification. It replaces + the timing information previously emitted when the `-debug` + command-line flag was set, and allows more fine-grained timing of + the native compiler + (`#11025 <https://github.com/coq/coq/pull/11025>`_, by Jason Gross). + Additionally, the timing information now uses real time rather than + user time (fixes `#11962 + <https://github.com/coq/coq/issues/11962>`_, `#11963 + <https://github.com/coq/coq/pull/11963>`_, by Jason Gross) +- **Changed:** + Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml + (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson). +- **Changed:** + Improve the efficiency of :tacn:`zify` by rewritting the remaining Ltac code in OCaml + (`#11429 <https://github.com/coq/coq/pull/11429>`_, by Frédéric Besson). +- **Changed:** + Backtrace information for tactics has been improved + (`#11755 <https://github.com/coq/coq/pull/11755>`_, + by Emilio Jesus Gallego Arias). +- **Changed:** + The default tactic used by :g:`firstorder` is + :g:`auto with core` instead of :g:`auto with *`; + see :ref:`decisionprocedures` for details; + old behavior can be reset by using the `-compat 8.12` command-line flag; + to ease the migration of legacy code, the default solver can be set to `debug auto with *` + with `Set Firstorder Solver debug auto with *` + (`#11760 <https://github.com/coq/coq/pull/11760>`_, + by Vincent Laporte). +- **Changed:** + :tacn:`autounfold` no longer fails when the :cmd:`Opaque` + command is used on constants in the hint databases + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + by Attila Gáspár). +- **Changed:** + Tactics with qualified name of the form ``Coq.Init.Notations`` are + now qualified with prefix ``Coq.Init.Ltac``; users of the ``-noinit`` + option should now import ``Coq.Init.Ltac`` if they want to use Ltac + (`#12023 <https://github.com/coq/coq/pull/12023>`_, + by Hugo Herbelin; minor source of incompatibilities). +- **Changed:** + Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is + indirectly dependent in the goal; the incompatibility can generally + be fixed by first clearing the hypotheses causing an indirect + dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`... in *` + instead; similarly, :tacn:`subst` has no more effect on such variables + (`#12146 <https://github.com/coq/coq/pull/12146>`_, + by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_ + and `#12139 <https://github.com/coq/coq/pull/12139>`_). +- **Changed:** + The check that :tacn:`unfold` arguments were indeed unfoldable has been moved to runtime + (`#12256 <https://github.com/coq/coq/pull/12256>`_, + by Pierre-Marie Pédrot; fixes + `#5764 <https://github.com/coq/coq/issues/5764>`_, + `#5159 <https://github.com/coq/coq/issues/5159>`_, + `#4925 <https://github.com/coq/coq/issues/4925>`_ + and `#11727 <https://github.com/coq/coq/issues/11727>`_). +- **Changed** + When the tactic :tacn:`functional induction` :n:`c__1 c__2 ... c__n` is used + with no parenthesis around :n:`c__1 c__2 ... c__n`, :n:`c__1 c__2 ... c__n` is now + read as one single applicative term. In particular implicit + arguments should be omitted. Rare source of incompatibility + (`#12326 <https://github.com/coq/coq/pull/12326>`_, + by Pierre Courtieu). +- **Changed:** + When using :tacn:`exists` or :tacn:`eexists` with multiple arguments, + the evaluation of arguments and applications of constructors are now interleaved. + This improves unification in some cases + (`#12366 <https://github.com/coq/coq/pull/12366>`_, + fixes `#12365 <https://github.com/coq/coq/issues/12365>`_, + by Attila Gáspár). +- **Removed:** + Undocumented ``omega with``. Using :tacn:`lia` is the recommended + replacement, although the old semantics of ``omega with *`` can also + be recovered with ``zify; omega`` + (`#11288 <https://github.com/coq/coq/pull/11288>`_, + by Emilio Jesus Gallego Arias). +- **Removed:** + Deprecated syntax `_eqn` for :tacn:`destruct` and :tacn:`remember`. + Use `eqn:` syntax instead + (`#11877 <https://github.com/coq/coq/pull/11877>`_, + by Hugo Herbelin). +- **Removed:** + `at` clauses can no longer be used with :tacn:`autounfold`. + Since they had no effect, it is safe to remove them + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + by Attila Gáspár). +- **Deprecated:** + The :tacn:`omega` tactic is deprecated; + use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead + (`#11976 <https://github.com/coq/coq/pull/11976>`_, + by Vincent Laporte). +- **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`) + are also added to help users to declare new :tacn:`zify` class instances using + Micromega tactics + (`#10998 <https://github.com/coq/coq/pull/10998>`_, by Kazuhiko Sakaguchi). +- **Added:** + :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls + (`#11474 <https://github.com/coq/coq/pull/11474>`_, by Frédéric Besson). +- **Added:** + Syntax :tacn:`pose proof` :n:`(@ident:=@term)` as an alternative to + :tacn:`pose proof` :n:`@term as @ident`, following the model of + :tacn:`pose` :n:`(@ident:=@term)` + (`#11522 <https://github.com/coq/coq/pull/11522>`_, + by Hugo Herbelin). +- **Added:** + New tactical :tacn:`with_strategy` which behaves like the command + :cmd:`Strategy`, with effects local to the given tactic + (`#12129 <https://github.com/coq/coq/pull/12129>`_, by Jason Gross). +- **Added:** + The :tacn:`zify` tactic is now aware of `Nat.le`, `Nat.lt` and `Nat.eq` + (`#12213 <https://github.com/coq/coq/pull/12213>`_, by Frédéric Besson; + fixes `#12210 <https://github.com/coq/coq/issues/12210>`_). +- **Fixed:** + :tacn:`zify` now handles :g:`Z.pow_pos` by default. + In Coq 8.11, this was the case only when loading module + :g:`ZifyPow` because this triggered a regression of :tacn:`lia`. + The regression is now fixed, and the module kept only for compatibility + (`#11362 <https://github.com/coq/coq/pull/11362>`_, + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_, + by Frédéric Besson). +- **Fixed:** + Efficiency regression of :tacn:`lia` + (`#11474 <https://github.com/coq/coq/pull/11474>`_, + fixes `#11436 <https://github.com/coq/coq/issues/11436>`_, + by Frédéric Besson). +- **Fixed:** + The behavior of :tacn:`autounfold` no longer depends on the names of terms and modules + (`#11883 <https://github.com/coq/coq/pull/11883>`_, + fixes `#7812 <https://github.com/coq/coq/issues/7812>`_, + by Attila Gáspár). +- **Fixed:** + Wrong type error in tactic :tacn:`functional induction` + (`#12326 <https://github.com/coq/coq/pull/12326>`_, + by Pierre Courtieu, + fixes `#11761 <https://github.com/coq/coq/issues/11761>`_, + reported by Lasse Blaauwbroek). + +Tactic language +^^^^^^^^^^^^^^^ + +- **Changed:** + The "reference" tactic generic argument now accepts arbitrary + variables of the goal context + (`#12254 <https://github.com/coq/coq/pull/12254>`_, + by Pierre-Marie Pédrot). +- **Added:** + An array library for Ltac2 (as compatible as possible with OCaml standard library) + (`#10343 <https://github.com/coq/coq/pull/10343>`_, + by Michael Soegtrop). +- **Added:** + The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to + give a name to the old value so as to be able to reuse it inside the + new one + (`#11503 <https://github.com/coq/coq/pull/11503>`_, + by Pierre-Marie Pédrot). +- **Added:** + Ltac2 notations for :tacn:`enough` and :tacn:`eenough` + (`#11740 <https://github.com/coq/coq/pull/11740>`_, + by Michael Soegtrop). +- **Added:** + New Ltac2 function ``Fresh.Free.of_goal`` to return the list of + names of declarations of the current goal; new Ltac2 function + ``Fresh.in_goal`` to return a variable fresh in the current goal + (`#11882 <https://github.com/coq/coq/pull/11882>`_, + by Hugo Herbelin). +- **Added:** + Ltac2 notations for reductions in terms: :n:`eval @red_expr in @ltac2_term` + (`#11981 <https://github.com/coq/coq/pull/11981>`_, + by Michael Soegtrop). +- **Fixed:** + The :flag:`Ltac Profiling` machinery now correctly handles + backtracking into multi-success tactics. The call-counts of some + tactics are unfortunately inflated by 1, as some tactics are + implicitly implemented as :g:`tac + fail`, which has two + entry-points rather than one (fixes `#12196 + <https://github.com/coq/coq/issues/12196>`_, `#12197 + <https://github.com/coq/coq/pull/12197>`_, by Jason Gross). + +SSReflect +^^^^^^^^^ + +- **Changed:** The :cmd:`Search (ssreflect)` command that used to be + available when loading the `ssreflect` plugin has been moved to a + separate plugin that needs to be loaded separately: `ssrsearch` + (part of `#8855 <https://github.com/coq/coq/pull/8855>`_, fixes + `#12253 <https://github.com/coq/coq/issues/12253>`_, by Théo + Zimmermann). +- **Deprecated:** :cmd:`Search (ssreflect)` (available through + `Require ssrsearch.`) in favor of the `headconcl:` clause of + :cmd:`Search` (part of `#8855 + <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann). + +Flags, options and attributes +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** :term:`Legacy attributes <attribute>` can now be passed + in any order (`#11665 <https://github.com/coq/coq/pull/11665>`_, by + Théo Zimmermann). +- **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). +- **Removed:** Deprecated unsound compatibility ``Template Check`` + flag that was introduced in 8.10 to help users gradually move their + template polymorphic inductive type definitions outside sections + (`#11546 <https://github.com/coq/coq/pull/11546>`_, by Pierre-Marie + Pédrot). +- **Removed:** + Deprecated ``Shrink Obligations`` flag + (`#11828 <https://github.com/coq/coq/pull/11828>`_, + by Emilio Jesus Gallego Arias). +- **Removed:** + Unqualified ``polymorphic``, ``monomorphic``, ``template``, + ``notemplate`` attributes (they were deprecated since Coq 8.10). + Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, + :attr:`universes(template)` and :attr:`universes(notemplate)` instead + (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). +- **Deprecated:** + :flag:`Hide Obligations` flag + (`#11828 <https://github.com/coq/coq/pull/11828>`_, + by Emilio Jesus Gallego Arias). +- **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical + Structure` declarations (`#11162 + <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). +- **Added:** + New attributes supported when defining an inductive type + :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`private(matching)`, which correspond to legacy attributes + ``Cumulative``, ``NonCumulative``, and the previously undocumented + ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by + Théo Zimmermann). +- **Added:** + The :cmd:`Hint` commands now accept the :attr:`export` locality as + an attribute, allowing to make import-scoped hints + (`#11812 <https://github.com/coq/coq/pull/11812>`_, + by Pierre-Marie Pédrot). +- **Added:** + :flag:`Cumulative StrictProp` to control cumulativity of |SProp| + (`#12034 <https://github.com/coq/coq/pull/12034>`_, by Gaëtan + Gilbert). + +Commands +^^^^^^^^ + +- **Changed:** + The :cmd:`Coercion` command has been improved to check the coherence of the + inheritance graph. It checks whether a circular inheritance path of `C >-> C` + is convertible with the identity function or not, then report it as an + ambiguous path if it is not. The new mechanism does not report ambiguous + paths that are redundant with others. For example, checking the ambiguity of + `[f; g]` and `[f'; g]` is redundant with that of `[f]` and `[f']` thus will + not be reported + (`#11258 <https://github.com/coq/coq/pull/11258>`_, + by Kazuhiko Sakaguchi). +- **Changed:** + Several commands (:cmd:`Search`, :cmd:`About`, ...) now print the + implicit arguments in brackets when printing types (`#11795 + <https://github.com/coq/coq/pull/11795>`_, by Simon Boulier). +- **Changed:** + :cmd:`Redirect` now obeys the :opt:`Printing Width` and + :opt:`Printing Depth` options + (`#12358 <https://github.com/coq/coq/pull/12358>`_, + by Emilio Jesus Gallego Arias). +- **Removed:** + Recursive OCaml loadpaths are not supported anymore; the command + ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the + preferred one. We have also dropped support for the non-qualified + version of the :cmd:`Add LoadPath` command, that is to say, + the ``Add LoadPath dir`` version; now, + you must always specify a prefix now using ``Add Loadpath dir as Prefix`` + (`#11618 <https://github.com/coq/coq/pull/11618>`_, + by Emilio Jesus Gallego Arias). +- **Removed:** undocumented ``Chapter`` command. Use :cmd:`Section` + instead (`#11746 <https://github.com/coq/coq/pull/11746>`_, by Théo + Zimmermann). +- **Removed:** ``SearchAbout`` command that was deprecated since 8.5. + Use :cmd:`Search` instead + (`#11944 <https://github.com/coq/coq/pull/11944>`_, by Jim Fehrle). +- **Deprecated:** + Declaration of arbitrary terms as hints. Global references are now + preferred (`#7791 <https://github.com/coq/coq/pull/7791>`_, by + Pierre-Marie Pédrot). +- **Deprecated:** :cmd:`SearchHead` in favor of the new `headconcl:` + clause of :cmd:`Search` (part of `#8855 + <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann). +- **Added:** + :cmd:`Print Canonical Projections` can now take constants as + arguments and prints only the unification rules that involve or are + synthesized from the given constants (`#10747 + <https://github.com/coq/coq/pull/10747>`_, by Kazuhiko Sakaguchi). +- **Added:** A section variable introduced with :cmd:`Let` can be + declared as a :cmd:`Canonical Structure` (`#11164 + <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). +- **Added:** Support for universe bindings and universe contrainsts in + :cmd:`Let` definitions (`#11534 + <https://github.com/coq/coq/pull/11534>`_, by Théo Zimmermann). +- **Added:** Support for new clauses `hyp:`, `headhyp:`, `concl:`, + `headconcl:`, `head:` and `is:` in :cmd:`Search`. Support for + complex search queries combining disjunctions, conjunctions and + negations (`#8855 <https://github.com/coq/coq/pull/8855>`_, by Hugo + Herbelin, with ideas from Cyril Cohen and help from Théo + Zimmermann). +- **Fixed:** + A printing bug in the presence of elimination principles with local definitions + (`#12295 <https://github.com/coq/coq/pull/12295>`_, + by Hugo Herbelin; fixes `#12233 <https://github.com/coq/coq/pull/12233>`_). +- **Fixed:** + Anomalies with :cmd:`Show Proof` + (`#12296 <https://github.com/coq/coq/pull/12296>`_, + by Hugo Herbelin; fixes + `#12234 <https://github.com/coq/coq/pull/12234>`_). + +Tools +^^^^^ + +- **Changed:** + Internal options and behavior of ``coqdep``. ``coqdep`` + no longer works as a replacement for ``ocamldep``, thus ``.ml`` + files are not supported as input. Also, several deprecated options + have been removed: ``-w``, ``-D``, ``-mldep``, ``-prefix``, + ``-slash``, and ``-dumpbox``. Passing ``-boot`` to ``coqdep`` will + not load any path by default now, ``-R/-Q`` should be used instead + (`#11523 <https://github.com/coq/coq/pull/11523>`_ and + `#11589 <https://github.com/coq/coq/pull/11589>`_, + by Emilio Jesus Gallego Arias). +- **Changed:** + The order in which the require flags `-ri`, `-re`, `-rfrom`, etc. + and the option flags `-set`, `-unset` are given now matters. In + particular, it is now possible to interleave the loading of plugins + and the setting of options by choosing the right order for these + flags. The load flags `-l` and `-lv` are still processed afterward + for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and + `#12097 <https://github.com/coq/coq/pull/12097>`_, + by Lasse Blaauwbroek). +- **Changed:** + The ``cleanall`` target of a makefile generated by ``coq_makefile`` + now erases ``.lia.cache`` and ``.nia.cache`` (`#12006 + <https://github.com/coq/coq/pull/12006>`_, by Olivier Laurent). +- **Changed:** + The output of ``make TIMED=1`` (and therefore the timing targets + such as ``print-pretty-timed`` and ``print-pretty-timed-diff``) now + displays the full name of the output file being built, rather than + the stem of the rule (which was usually the filename without the + extension, but in general could be anything for user-defined rules + involving ``%``) (`#12126 + <https://github.com/coq/coq/pull/12126>`_, by Jason Gross). +- **Changed:** + When passing ``TIMED=1`` to ``make`` with either Coq's own makefile + or a ``coq_makefile``\-made makefile, timing information is now + printed for OCaml files as well (`#12211 + <https://github.com/coq/coq/pull/12211>`_, by Jason Gross). +- **Changed:** + The pretty-timed scripts and targets now print a newline at the end of their + tables, rather than creating text with no trailing newline (`#12368 + <https://github.com/coq/coq/pull/12368>`_, by Jason Gross). +- **Removed:** + The `-load-ml-source` and `-load-ml-object` command-line options + have been removed; their use was very limited, you can achieve the same adding + additional object files in the linking step or using a plugin + (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias). +- **Removed:** + The confusingly-named `-require` command-line option, which was + deprecated since 8.11. Use the equivalent `-require-import` / `-ri` + options instead + (`#12005 <https://github.com/coq/coq/pull/12005>`_, + by Théo Zimmermann). +- **Deprecated:** + ``-cumulative-sprop`` command-line flag in favor of the new + :flag:`Cumulative StrictProp` flag (`#12034 + <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert). +- **Added:** + A new documentation environment ``details`` to make certain portion + of a Coq document foldable. See :ref:`coqdoc-hide-show` + (`#10592 <https://github.com/coq/coq/pull/10592>`_, + by Thomas Letan). +- **Added:** + The ``make-both-single-timing-files.py`` script now accepts a + ``--fuzz=N`` parameter on the command line which determines how many + characters two lines may be offset in the "before" and "after" + timing logs while still being considered the same line. When + invoking this script via the ``print-pretty-single-time-diff`` + target in a ``Makefile`` made by ``coq_makefile``, you can set this + argument by passing ``TIMING_FUZZ=N`` to ``make`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). +- **Added:** + The ``make-one-time-file.py`` and ``make-both-time-files.py`` + scripts now accept a ``--real`` parameter on the command line to + print real times rather than user times in the tables. The + ``make-both-single-timing-files.py`` script accepts a ``--user`` + parameter to use user times. When invoking these scripts via the + ``print-pretty-timed`` or ``print-pretty-timed-diff`` or + ``print-pretty-single-time-diff`` targets in a ``Makefile`` made by + ``coq_makefile``, you can set this argument by passing + ``TIMING_REAL=1`` (to pass ``--real``) or ``TIMING_REAL=0`` (to pass + ``--user``) to ``make`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). +- **Added:** + Coq's build system now supports both ``TIMING_FUZZ``, + ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile`` + made by ``coq_makefile`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). +- **Added:** + The ``make-one-time-file.py`` and ``make-both-time-files.py`` + scripts now include peak memory usage information in the tables (can + be turned off by the ``--no-include-mem`` command-line parameter), + and a ``--sort-by-mem`` parameter to sort the tables by memory + rather than time. When invoking these scripts via the + ``print-pretty-timed`` or ``print-pretty-timed-diff`` targets in a + ``Makefile`` made by ``coq_makefile``, you can set this argument by + passing ``TIMING_INCLUDE_MEM=0`` (to pass ``--no-include-mem``) and + ``TIMING_SORT_BY_MEM=1`` (to pass ``--sort-by-mem``) to ``make`` + (`#11606 <https://github.com/coq/coq/pull/11606>`_, by Jason Gross). +- **Added:** + Coq's build system now supports both ``TIMING_INCLUDE_MEM`` and + ``TIMING_SORT_BY_MEM`` just like a ``Makefile`` made by + ``coq_makefile`` (`#11606 <https://github.com/coq/coq/pull/11606>`_, + by Jason Gross). +- **Added:** + New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the + `Coq` library prefix by default + (`#11617 <https://github.com/coq/coq/pull/11617>`_, + by Emilio Jesus Gallego Arias). +- **Added:** + Definitions in coqdoc link to themselves, giving access in html to their own url + (`#12026 <https://github.com/coq/coq/pull/12026>`_, + by Hugo Herbelin; granting `#7093 <https://github.com/coq/coq/pull/7093>`_). +- **Added:** + Hyperlinks on bound variables in coqdoc + (`#12033 <https://github.com/coq/coq/pull/12033>`_, + by Hugo Herbelin; it incidentally fixes + `#7697 <https://github.com/coq/coq/pull/7697>`_). +- **Added:** + Highlighting of link targets in coqdoc + (`#12091 <https://github.com/coq/coq/pull/12091>`_, + by Hugo Herbelin). +- **Fixed:** + The various timing targets for Coq's standard library now correctly + display and label the "before" and "after" columns, rather than + mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_ + fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason + Gross). +- **Fixed:** + The sorting order of the timing script ``make-both-time-files.py`` + and the target ``print-pretty-timed-diff`` is now deterministic even + when the sorting order is ``absolute`` or ``diff``; previously the + relative ordering of two files with identical times was + non-deterministic (`#11606 + <https://github.com/coq/coq/pull/11606>`_, by Jason Gross). +- **Fixed:** + Fields of a record tuple now link in coqdoc to their definition + (`#12027 <https://github.com/coq/coq/pull/12027>`_, fixes + `#3415 <https://github.com/coq/coq/issues/3415>`_, + by Hugo Herbelin). +- **Fixed:** + ``coqdoc`` now reports the location of a mismatched opening ``[[`` + instead of throwing an uninformative exception + (`#12037 <https://github.com/coq/coq/pull/12037>`_, + fixes `#9670 <https://github.com/coq/coq/issues/9670>`_, + by Xia Li-yao). +- **Fixed:** + coqchk incorrectly reporting names from opaque modules as axioms + (`#12076 <https://github.com/coq/coq/pull/12076>`_, + by Pierre Roux; fixes `#5030 <https://github.com/coq/coq/issues/5030>`_). +- **Fixed:** + coq_makefile-generated ``Makefile``\s ``pretty-timed-diff`` target + no longer raises Python exceptions in the rare corner case where the + log of times contains no files (`#12388 + <https://github.com/coq/coq/pull/12388>`_, fixes `#12387 + <https://github.com/coq/coq/pull/12387>`_, by Jason Gross). + +CoqIDE +^^^^^^ + +- **Removed:** + "Tactic" menu from CoqIDE which had been unmaintained for a number of years + (`#11414 <https://github.com/coq/coq/pull/11414>`_, + by Pierre-Marie Pédrot). +- **Removed:** + "Revert all buffers" command from CoqIDE which had been broken for a long time + (`#11415 <https://github.com/coq/coq/pull/11415>`_, + by Pierre-Marie Pédrot). + +Standard library +^^^^^^^^^^^^^^^^ + +- **Changed:** + Notations :n:`[|@term|]` and :n:`[||@term||]` for morphisms from 63-bit + integers to :g:`Z` and :g:`zn2z int` have been removed in favor of + :n:`φ(@term)` and :n:`Φ(@term)` respectively. These notations were + breaking Ltac parsing (`#11686 <https://github.com/coq/coq/pull/11686>`_, + by Maxime Dénès). +- **Changed:** + The names of ``Sorted_sort`` and ``LocallySorted_sort`` in ``Coq.Sorting.MergeSort`` + have been swapped to appropriately reflect their meanings + (`#11885 <https://github.com/coq/coq/pull/11885>`_, + by Lysxia). +- **Changed:** + Notations :g:`<=?` and :g:`<?` from ``Coq.Structures.Orders`` and + ``Coq.Sorting.Mergesort.NatOrder`` are now at level 70 rather than + 35, so as to be compatible with the notations defined everywhere + else in the standard library. This may require re-parenthesizing + some expressions. These notations were breaking the ability to + import modules from the standard library that were otherwise + compatible (fixes `#11890 + <https://github.com/coq/coq/issues/11890>`_, `#11891 + <https://github.com/coq/coq/pull/11891>`_, by Jason Gross). +- **Changed:** + The level of :g:`≡` in ``Coq.Numbers.Cyclic.Int63.Int63`` is now 70, + no associativity, in line with :g:`=`. Note that this is a minor + incompatibility with developments that declare their own :g:`≡` + notation and import ``Int63`` (fixes `#11905 + <https://github.com/coq/coq/issues/11905>`_, `#11909 + <https://github.com/coq/coq/pull/11909>`_, by Jason Gross). +- **Changed:** + No longer re-export ``ListNotations`` from ``Program`` (``Program.Syntax``) + (`#11992 <https://github.com/coq/coq/pull/11992>`_, + by Antonio Nikishaev). +- **Changed:** + It is now possible to import the :g:`nsatz` machinery without + transitively depending on the axioms of the real numbers nor of + classical logic by loading ``Coq.nsatz.NsatzTactic`` rather than + ``Coq.nsatz.Nsatz``. Note that some constants have changed kernel + names, living in ``Coq.nsatz.NsatzTactic`` rather than + ``Coq.nsatz.Nsatz``; this might cause minor incompatibilities that + can be fixed by actually running :g:`Import Nsatz` rather than + relying on absolute names (`#12073 + <https://github.com/coq/coq/pull/12073>`_, by Jason Gross; fixes + `#5445 <https://github.com/coq/coq/issues/5445>`_). +- **Changed:** + new lemma ``NoDup_incl_NoDup`` in ``List.v`` + to remove useless hypothesis `NoDup l'` in ``Sorting.Permutation.NoDup_Permutation_bis`` + (`#12120 <https://github.com/coq/coq/pull/12119>`_, + by Olivier Laurent). +- **Changed:** + :cmd:`Fixpoints <Fixpoint>` of the standard library without a recursive call turned + into ordinary :cmd:`Definitions <Definition>` + (`#12121 <https://github.com/coq/coq/pull/12121>`_, + by Hugo Herbelin; fixes `#11903 <https://github.com/coq/coq/pull/11903>`_). +- **Deprecated:** + ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le`` + is made local to avoid conflicts with ``Nat.le``. As a consequence, + previous calls to ``leb`` based on importing ``Bool`` should now be + qualified into ``Bool.le`` even if ``Bool`` is imported + (`#12162 <https://github.com/coq/coq/pull/12162>`_, + by Olivier Laurent). +- **Added:** Theorem :g:`bezout_comm` for natural numbers + (`#11127 <https://github.com/coq/coq/pull/11127>`_, by Daniel de Rauglaudre). +- **Added** + :g:`rew dependent` notations for the dependent version of + :g:`rew` in :g:`Coq.Init.Logic.EqNotations` to improve the display + and parsing of :g:`match` statements on :g:`Logic.eq` (`#11240 + <https://github.com/coq/coq/pull/11240>`_, by Jason Gross). +- **Added:** + Lemmas about lists: + + - properties of ``In``: ``in_elt``, ``in_elt_inv`` + - properties of ``nth``: ``app_nth2_plus``, ``nth_middle``, ``nth_ext`` + - properties of ``last``: ``last_last``, ``removelast_last`` + - properties of ``remove``: ``remove_cons``, ``remove_app``, ``notin_remove``, ``in_remove``, ``in_in_remove``, ``remove_remove_comm``, ``remove_remove_eq``, ``remove_length_le``, ``remove_length_lt`` + - properties of ``concat``: ``in_concat``, ``remove_concat`` + - properties of ``map`` and ``flat_map``: ``map_last``, ``map_eq_cons``, ``map_eq_app``, ``flat_map_app``, ``flat_map_ext``, ``nth_nth_nth_map`` + - properties of ``incl``: ``incl_nil_l``, ``incl_l_nil``, ``incl_cons_inv``, ``incl_app_app``, ``incl_app_inv``, ``remove_incl``, ``incl_map``, ``incl_filter``, ``incl_Forall_in_iff`` + - properties of ``NoDup`` and ``nodup``: ``NoDup_rev``, ``NoDup_filter``, ``nodup_incl`` + - properties of ``Exists`` and ``Forall``: ``Exists_nth``, ``Exists_app``, ``Exists_rev``, ``Exists_fold_right``, ``incl_Exists``, ``Forall_nth``, ``Forall_app``, ``Forall_elt``, ``Forall_rev``, ``Forall_fold_right``, ``incl_Forall``, ``map_ext_Forall``, ``Exists_or``, ``Exists_or_inv``, ``Forall_and``, ``Forall_and_inv``, ``exists_Forall``, ``Forall_image``, ``concat_nil_Forall``, ``in_flat_map_Exists``, ``notin_flat_map_Forall`` + - properties of ``repeat``: ``repeat_cons``, ``repeat_to_concat`` + - definitions and properties of ``list_sum`` and ``list_max``: ``list_sum_app``, ``list_max_app``, ``list_max_le``, ``list_max_lt`` + - misc: ``elt_eq_unit``, ``last_length``, ``rev_eq_app``, ``removelast_firstn_len``, ``cons_seq``, ``seq_S`` + + (`#11249 <https://github.com/coq/coq/pull/11249>`_, `#12237 <https://github.com/coq/coq/pull/12237>`_, + by Olivier Laurent). +- **Added:** + Well-founded induction principles for `nat`: ``lt_wf_rect1``, ``lt_wf_rect``, ``gt_wf_rect``, ``lt_wf_double_rect`` + (`#11335 <https://github.com/coq/coq/pull/11335>`_, + by Olivier Laurent). +- **Added:** + ``remove'`` and ``count_occ'`` over lists, + alternatives to ``remove`` and ``count_occ`` based on ``filter`` + (`#11350 <https://github.com/coq/coq/pull/11350>`_, + by Yishuai Li). +- **Added:** + Facts about ``N.iter`` and ``Pos.iter``: + + - ``N.iter_swap_gen``, ``N.iter_swap``, ``N.iter_succ``, ``N.iter_succ_r``, ``N.iter_add``, ``N.iter_ind``, ``N.iter_invariant``; + - ``Pos.iter_succ_r``, ``Pos.iter_ind``. + + (`#11880 <https://github.com/coq/coq/pull/11880>`_, + by Lysxia). +- **Added:** + Facts about ``Permutation``: + + - structure: ``Permutation_refl'``, ``Permutation_morph_transp`` + - compatibilities: ``Permutation_app_rot``, ``Permutation_app_swap_app``, ``Permutation_app_middle``, ``Permutation_middle2``, ``Permutation_elt``, ``Permutation_Forall``, ``Permutation_Exists``, ``Permutation_Forall2``, ``Permutation_flat_map``, ``Permutation_list_sum``, ``Permutation_list_max`` + - inversions: ``Permutation_app_inv_m``, ``Permutation_vs_elt_inv``, ``Permutation_vs_cons_inv``, ``Permutation_vs_cons_cons_inv``, ``Permutation_map_inv``, ``Permutation_image``, ``Permutation_elt_map_inv`` + - length-preserving definition by means of transpositions ``Permutation_transp`` with associated properties: ``Permutation_transp_sym``, ``Permutation_transp_equiv``, ``Permutation_transp_cons``, ``Permutation_Permutation_transp``, ``Permutation_ind_transp`` + + (`#11946 <https://github.com/coq/coq/pull/11946>`_, + by Olivier Laurent). +- **Added:** + Notations for sigma types: ``{ x & P & Q }``, ``{ ' pat & P }``, ``{ ' pat & P & Q }`` + (`#11957 <https://github.com/coq/coq/pull/11957>`_, + by Olivier Laurent). +- **Added:** + Order relations ``lt`` and ``compare`` added in ``Bool.Bool``. + Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx`` + (`#12008 <https://github.com/coq/coq/pull/12008>`_, + by Olivier Laurent). +- **Added:** + Properties of some operations on vectors: + + - ``nth_order``: ``nth_order_hd``, ``nth_order_tl``, ``nth_order_ext`` + - ``replace``: ``nth_order_replace_eq``, ``nth_order_replace_neq``, ``replace_id``, ``replace_replace_eq``, ``replace_replace_neq`` + - ``map``: ``map_id``, ``map_map``, ``map_ext_in``, ``map_ext`` + - ``Forall`` and ``Forall2``: ``Forall_impl``, ``Forall_forall``, ``Forall_nth_order``, ``Forall2_nth_order`` + + (`#12014 <https://github.com/coq/coq/pull/12014>`_, + by Olivier Laurent). +- **Added:** + Lemmas + :g:`orb_negb_l`, + :g:`andb_negb_l`, + :g:`implb_true_iff`, + :g:`implb_false_iff`, + :g:`implb_true_r`, + :g:`implb_false_r`, + :g:`implb_true_l`, + :g:`implb_false_l`, + :g:`implb_same`, + :g:`implb_contrapositive`, + :g:`implb_negb`, + :g:`implb_curry`, + :g:`implb_andb_distrib_r`, + :g:`implb_orb_distrib_r`, + :g:`implb_orb_distrib_l` in library :g:`Bool` + (`#12018 <https://github.com/coq/coq/pull/12018>`_, + by Hugo Herbelin). +- **Added:** + Definition and properties of cyclic permutations / circular shifts: ``CPermutation`` + (`#12031 <https://github.com/coq/coq/pull/12031>`_, + by Olivier Laurent). +- **Added:** + ``Structures.OrderedTypeEx.Ascii_as_OT`` + (`#12044 <https://github.com/coq/coq/pull/12044>`_, + by formalize.eth (formalize@protonmail.com)). +- **Fixed:** + Rewrote ``Structures.OrderedTypeEx.String_as_OT.compare`` + to avoid huge proof terms + (`#12044 <https://github.com/coq/coq/pull/12044>`_, + by formalize.eth (formalize@protonmail.com); + fixes `#12015 <https://github.com/coq/coq/issues/12015>`_). + +Reals library +^^^^^^^^^^^^^ + +- **Changed:** + Cleanup of names in the Reals theory: replaced `tan_is_inj` with + `tan_inj` and replaced `atan_right_inv` with `tan_atan` - + compatibility notations are provided. Moved various auxiliary lemmas + from `Ratan.v` to more appropriate places + (`#9803 <https://github.com/coq/coq/pull/9803>`_, + by Laurent Théry and Michael Soegtrop). +- **Changed:** + Replace `CRzero` and `CRone` by `CR_of_Q 0` and `CR_of_Q 1` in + `ConstructiveReals`. Use implicit arguments for + `ConstructiveReals`. Move `ConstructiveReals` into new directory + `Abstract`. Remove imports of implementations inside those + `Abstract` files. Move implementation by means of Cauchy sequences + in new directory `Cauchy`. Split files `ConstructiveMinMax` and + `ConstructivePower`. + + .. warning:: The constructive reals modules are marked as experimental. + + (`#11725 <https://github.com/coq/coq/pull/11725>`_, + `#12287 <https://github.com/coq/coq/pull/12287>`_ + and `#12288 <https://github.com/coq/coq/pull/12288>`_, + by Vincent Semeria). +- **Removed:** + Type `RList` has been removed. All uses have been replaced by `list R`. + Functions from `RList` named `In`, `Rlength`, `cons_Rlist`, `app_Rlist` + have also been removed as they are essentially the same as `In`, `length`, + `app`, and `map` from `List`, modulo the following changes: + + - `RList.In x (RList.cons a l)` used to be convertible to + `(x = a) \\/ RList.In x l`, + but `List.In x (a :: l)` is convertible to + `(a = x) \\/ List.In l`. + The equality is reversed. + - `app_Rlist` and `List.map` take arguments in different order. + + (`#11404 <https://github.com/coq/coq/pull/11404>`_, + by Yves Bertot). +- **Added:** + inverse trigonometric functions `asin` and `acos` with lemmas for + the derivatives, bounds and special values of these functions; an + extensive set of identities between trigonometric functions and + their inverse functions; lemmas for the injectivity of sine and + cosine; lemmas on the derivative of the inverse of decreasing + functions and on the derivative of horizontally mirrored functions; + various generic auxiliary lemmas and definitions for `Rsqr`, `sqrt`, + `posreal` and others + (`#9803 <https://github.com/coq/coq/pull/9803>`_, + by Laurent Théry and Michael Soegtrop). + +Extraction +^^^^^^^^^^ + +- **Added:** + Support for better extraction of strings in OCaml and Haskell: + `ExtOcamlNativeString` provides bindings from the Coq `String` type to + the OCaml `string` type, and string literals can be extracted to literals, + both in OCaml and Haskell (`#10486 + <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from + Maxime Dénès, review by Hugo Herbelin). +- **Fixed:** + In Haskell extraction with ``ExtrHaskellString``, equality comparisons on + strings and characters are now guaranteed to be uniquely well-typed, even in + very polymorphic contexts under ``unsafeCoerce``; this is achieved by adding + type annotations to the extracted code, and by making ``ExtrHaskellString`` + export ``ExtrHaskellBasic`` (`#12263 + <https://github.com/coq/coq/pull/12263>`_, by Jason Gross, fixes `#12257 + <https://github.com/coq/coq/issues/12257>`_ and `#12258 + <https://github.com/coq/coq/issues/12258>`_). + +Reference manual +^^^^^^^^^^^^^^^^ + +- **Changed:** + The reference manual has been restructured to get a more logical + organization. In the new version, there are fewer top-level + chapters, and, in the HTML format, chapters are split into smaller + pages. This is still a work in progress and further restructuring + is expected in the next versions of Coq + (`CEP#43 <https://github.com/coq/ceps/pull/43>`_, implemented in + `#11601 <https://github.com/coq/coq/pull/11601>`_, + `#11871 <https://github.com/coq/coq/pull/11871>`_, + `#11914 <https://github.com/coq/coq/pull/11914>`_, + `#12148 <https://github.com/coq/coq/pull/12148>`_, + `#12172 <https://github.com/coq/coq/pull/12172>`_, + `#12239 <https://github.com/coq/coq/pull/12239>`_ + and `#12330 <https://github.com/coq/coq/pull/12330>`_, + effort inspired by Matthieu Sozeau, led by Théo Zimmermann, with + help and reviews of Jim Fehrle, Clément Pit-Claudel and others). +- **Changed:** + Most of the grammar is now presented using the notation mechanism + that has been used to present commands and tactics since Coq 8.8 and + which is documented in :ref:`syntax-conventions` + (`#11183 <https://github.com/coq/coq/pull/11183>`_, + `#11314 <https://github.com/coq/coq/pull/11314>`_, + `#11423 <https://github.com/coq/coq/pull/11423>`_, + `#11705 <https://github.com/coq/coq/pull/11705>`_, + `#11718 <https://github.com/coq/coq/pull/11718>`_, + `#11720 <https://github.com/coq/coq/pull/11720>`_ + and `#11961 <https://github.com/coq/coq/pull/11961>`_, by Jim + Fehrle, reviewed by Théo Zimmermann). +- **Added:** + A glossary of terms and an index of attributes + (`#11869 <https://github.com/coq/coq/pull/11869>`_, + `#12150 <https://github.com/coq/coq/pull/12150>`_ + and `#12224 <https://github.com/coq/coq/pull/12224>`_, + by Jim Fehrle and Théo Zimmermann, + reviewed by Clément Pit-Claudel) +- **Added:** + A selector that allows switching between versions of the reference + manual (`#12286 <https://github.com/coq/coq/pull/12286>`_, by + Clément Pit-Claudel). +- **Fixed:** + Most of the documented syntax has been thoroughly updated to make it + accurate and easily understood. This was done using a + semi-automated `doc_grammar` tool introduced for this purpose and + through significant revisions to the text + (`#9884 <https://github.com/coq/coq/pull/9884>`_, + `#10614 <https://github.com/coq/coq/pull/10614>`_, + `#11314 <https://github.com/coq/coq/pull/11314>`_, + `#11423 <https://github.com/coq/coq/pull/11423>`_, + `#11705 <https://github.com/coq/coq/pull/11705>`_, + `#11718 <https://github.com/coq/coq/pull/11718>`_, + `#11720 <https://github.com/coq/coq/pull/11720>`_ + `#11797 <https://github.com/coq/coq/pull/11797>`_, + `#11913 <https://github.com/coq/coq/pull/11913>`_, + `#11958 <https://github.com/coq/coq/pull/11958>`_ + `#11960 <https://github.com/coq/coq/pull/11960>`_ + and `#11961 <https://github.com/coq/coq/pull/11961>`_, by Jim + Fehrle, reviewed by Théo Zimmermann). + +Infrastructure and dependencies +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + Minimal versions of dependencies for building the reference manual: + now requires Sphinx 2.3.1+, sphinx_rtd_theme 0.4.3+ and + sphinxcontrib-bibtex 0.4.2+ + (`#12224 <https://github.com/coq/coq/pull/12224>`_, + by Jim Fehrle and Théo Zimmermann). +- **Removed:** + Python 2 is no longer required in any part of the codebase + (`#11245 <https://github.com/coq/coq/pull/11245>`_, + by Emilio Jesus Gallego Arias). + Version 8.11 ------------ diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 68900aa0be..8918e87180 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -15,6 +15,8 @@ settings that |Coq| provides. Syntax and lexical conventions ------------------------------ +.. _syntax-conventions: + Syntax conventions ~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 408f8fc3ec..33ebbce640 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -170,6 +170,10 @@ Here we describe only few of them. override the flags passed to ``coqdoc``. By default ``-interpolate -utf8``. :COQDOCEXTRAFLAGS: extend the flags passed to ``coqdoc`` +:COQLIBINSTALL, COQDOCINSTALL: + specify where the Coq libraries and documentation will be installed. + By default a combination of ``$(DESTDIR)`` (if defined) with + ``$(COQLIB)/user-contrib`` and ``$(DOCDIR)/user-contrib``. **Rule extension** diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index b4b14fb392..f872c1b2e3 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -220,8 +220,10 @@ Identifiers from the |Coq| standard library are linked to the Coq website using command line options ``--no-externals`` and ``--coqlib``; see below. -Hiding / Showing parts of the source. -+++++++++++++++++++++++++++++++++++++ +.. _coqdoc-hide-show: + +Hiding / Showing parts of the source +++++++++++++++++++++++++++++++++++++ Some parts of the source can be hidden using command line options ``-g`` and ``-l`` (see below), or using such comments: diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index b4527694ae..2e72ceae5a 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -114,11 +114,6 @@ END (** Eauto *) -TACTIC EXTEND prolog DEPRECATED { Deprecation.make ~note:"Use eauto instead" () } -| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> - { Eauto.prolog_tac (eval_uconstrs ist l) n } -END - { let make_depth n = snd (Eauto.make_dimension n None) diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg index 6d68cc13ab..f5cbf2005b 100644 --- a/plugins/ssrsearch/g_search.mlg +++ b/plugins/ssrsearch/g_search.mlg @@ -2,6 +2,8 @@ (* Main prefilter *) +DECLARE PLUGIN "ssrsearch_plugin" + { module CoqConstr = Constr diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 5e3fb9dae3..25353b7c12 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1716,7 +1716,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = let flags = (default_flags_of TransparentState.full) in match solve_simple_eqn evar_unify flags !!env sigma (None,ev,substl inst ev') with | Success evd -> evdref := evd - | UnifFailure _ -> assert false + | UnifFailure _ -> evdref := add_conv_pb (Reduction.CONV,!!env,substl inst ev',t) sigma end; ev' | _ -> diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 710e0a6808..7d8620468d 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -77,31 +77,6 @@ let apply_tac_list tac glls = re_sig (pack.it @ rest) pack.sigma | _ -> user_err Pp.(str "apply_tac_list") -let one_step l gl = - [Proofview.V82.of_tactic Tactics.intro] - @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl))) - @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l) - @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl)) - -let rec prolog l n gl = - if n <= 0 then user_err Pp.(str "prolog - failure"); - let prol = (prolog l (n-1)) in - (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl - -let prolog_tac l n = - Proofview.V82.tactic begin fun gl -> - let map c = - let (sigma, c) = c (pf_env gl) (project gl) in - (* Dropping the universe context is probably wrong *) - let (c, _) = pf_apply (prepare_hint false) gl (sigma, c) in - c - in - let l = List.map map l in - try (prolog l n gl) - with UserError (Some "Refiner.tclFIRST",_) -> - user_err ~hdr:"Prolog.prolog" (str "Prolog failed.") - end - open Auto (***************************************************************************) diff --git a/tactics/eauto.mli b/tactics/eauto.mli index e6f2c1a8e2..5fb038a767 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -18,8 +18,6 @@ val registered_e_assumption : unit Proofview.tactic val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic -val prolog_tac : delayed_open_constr list -> int -> unit Proofview.tactic - val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/bug_12418.v b/test-suite/bugs/closed/bug_12418.v new file mode 100644 index 0000000000..cf11ea627b --- /dev/null +++ b/test-suite/bugs/closed/bug_12418.v @@ -0,0 +1,29 @@ +(* The second "match" below used to raise an anomaly *) + +Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type := + { ret : forall {t : Type@{d}}, t -> m t }. + +Record state {S : Type} (t : Type) : Type := mkState { runState : t }. + +Global Declare Instance Monad_state : forall S, Monad (@state S). + +Class Cava := { + constant : bool -> unit; + constant_vec : unit; +}. + +Axiom F : forall {A : Type}, (bool -> A) -> Datatypes.unit. + +Fail Instance T : Cava := { + + constant b := match b with + | true => ret tt + | false => ret tt + end; + + constant_vec := @F _ (fun b => match b with + | true => tt + | false => tt + end); + +}. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh new file mode 100755 index 0000000000..4a50759bdb --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +set -x +set -e + +cd "$(dirname "${BASH_SOURCE[0]}")" + +"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both.log + +diff -u time-of-build-both.log.expected time-of-build-both.log || exit $? diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in new file mode 100644 index 0000000000..1031cb85c5 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in @@ -0,0 +1,58 @@ +./src/Rewriter/PerfTesting/Specific/make.py primes.txt +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +coq_makefile -f _CoqProject INSTALLDEFAULTROOT = Crypto -o Makefile-coq +COQ_MAKEFILE -f _CoqProject > Makefile.coq +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +COQDEP VFILES +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +COQC src/UnsaturatedSolinasHeuristics/Tests.v +Finished transaction in 25.269 secs (24.869u,0.051s) (successful) +src/UnsaturatedSolinasHeuristics/Tests.vo (real: 26.27, user: 25.97, sys: 0.27, mem: 566428 ko) +DIFF Crypto.Fancy.Montgomery256.Prod.MontRed256 +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct.Assumptions +DIFF Crypto.Fancy.Montgomery256.montred256 +DIFF Crypto.Fancy.Barrett256.Prod.MulMod +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions +DIFF Crypto.Fancy.Barrett256.barrett_red256 +DIFF Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs +cp -f AUTHORS fiat-rust/AUTHORS +cp -f CONTRIBUTORS fiat-rust/CONTRIBUTORS +cp -f LICENSE fiat-rust/LICENSE diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in new file mode 100644 index 0000000000..b78039b589 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in @@ -0,0 +1,40 @@ +./src/Rewriter/PerfTesting/Specific/make.py primes.txt +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +coq_makefile -f _CoqProject INSTALLDEFAULTROOT = Crypto -o Makefile-coq +COQ_MAKEFILE -f _CoqProject > Makefile.coq +make --no-print-directory -C rewriter +make[2]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/deps/coqutil +Generating Makefile.coq.all +make -f Makefile.coq.all +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C bedrock2/bedrock2 noex +Generating Makefile.coq.noex +rm -f .coqdeps.d +make -f Makefile.coq.noex +make[3]: Nothing to be done for 'real-all'. +make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo +make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date. +DIFF Crypto.Fancy.Montgomery256.Prod.MontRed256 +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct +DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct.Assumptions +DIFF Crypto.Fancy.Montgomery256.montred256 +DIFF Crypto.Fancy.Barrett256.Prod.MulMod +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct +DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions +DIFF Crypto.Fancy.Barrett256.barrett_red256 +cp -f AUTHORS fiat-rust/AUTHORS +cp -f CONTRIBUTORS fiat-rust/CONTRIBUTORS +cp -f LICENSE fiat-rust/LICENSE diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected new file mode 100644 index 0000000000..6a232623bf --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected @@ -0,0 +1,5 @@ + After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) +------------------------------------------------------------------------------------------------------------------------------------------- +0m25.96s | 566428 ko | Total Time / Peak Mem | 0m00.00s | 0 ko || +0m25.96s || 566428 ko | N/A | ∞ +------------------------------------------------------------------------------------------------------------------------------------------- +0m25.97s | 566428 ko | UnsaturatedSolinasHeuristics/Tests.vo | N/A | N/A || +0m25.96s || 566428 ko | ∞ | ∞ diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh index 8935759705..123b272a69 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh @@ -12,3 +12,4 @@ export COQLIB ./003-non-utf8/run.sh ./004-per-file-fuzz/run.sh ./005-correct-diff-sorting-order-mem/run.sh +./006-zero-before/run.sh diff --git a/test-suite/output/ErrorLocation_12152_1.v b/test-suite/output/ErrorLocation_12152_1.v index e63ab1cd48..709ac305e4 100644 --- a/test-suite/output/ErrorLocation_12152_1.v +++ b/test-suite/output/ErrorLocation_12152_1.v @@ -1,3 +1,4 @@ (* Reported in #12152 *) Goal True. intro H; auto. +Abort. diff --git a/test-suite/output/ErrorLocation_12152_2.v b/test-suite/output/ErrorLocation_12152_2.v index 5df6bec939..29e4c910d8 100644 --- a/test-suite/output/ErrorLocation_12152_2.v +++ b/test-suite/output/ErrorLocation_12152_2.v @@ -1,3 +1,4 @@ (* Reported in #12152 *) Goal True. intros H; auto. +Abort. diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v index 347424b2fc..59c0e1dfc5 100644 --- a/test-suite/output/ErrorLocation_12255.v +++ b/test-suite/output/ErrorLocation_12255.v @@ -2,3 +2,4 @@ Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac. Definition i := O. Goal False. can_unfold (i>0). +Abort. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index a26eb9dfbe..e2ed2db728 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -146,6 +146,21 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line TGTS ?= +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) +endif + +# Substitution of the path by appending $(DESTDIR) if needed. +# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. +windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) +destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) + +# Installation paths of libraries and documentation. +COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) +COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/user-contrib) +COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? + ########## End of parameters ################################################## # What follows may be relevant to you only if you need to # extend this Makefile. If so, look for 'Extension point' here and @@ -227,17 +242,6 @@ else TIMING_ARG= endif -# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) -ifdef DSTROOT -DESTDIR := $(DSTROOT) -endif - -concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2)) - -COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib) -COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib) -COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop) - # Files ####################################################################### # # We here define a bunch of variables about the files being part of the @@ -577,7 +581,7 @@ uninstall:: instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ rm -f "$$instf" &&\ echo RM "$$instf" &&\ - (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ + (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ done .PHONY: uninstall diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index a3078af4a1..12462726e5 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -387,8 +387,8 @@ def make_diff_table_string(left_dict, right_dict, total_string = 'Total' if not include_mem else 'Total Time / Peak Mem' middle_width = max(map(len, names + [tag, total_string])) - left_peak = max(v.get(MEM_KEY, 0) for v in left_dict.values()) - right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values()) + left_peak = max([0] + [v.get(MEM_KEY, 0) for v in left_dict.values()]) + right_peak = max([0] + [v.get(MEM_KEY, 0) for v in right_dict.values()]) diff_peak = left_peak - right_peak percent_diff_peak = (format_percentage((left_peak - right_peak) / float(right_peak)) if right_peak != 0 else (INFINITY if left_peak > 0 else 'N/A')) diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 8979170026..3af39ec59a 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +DECLARE PLUGIN "ltac2_plugin" + { open Pp diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 80ca85e9a6..0b75e7f410 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -285,7 +285,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let fix_kind = Decls.IsDefinition fix_kind in let _ : GlobRef.t list = Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx - ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration + ~possible_indexes:indexes ~udecl ~ntns ~rec_declaration fixitems in () diff --git a/vernac/declare.ml b/vernac/declare.ml index c77d4909da..6ed7a9e39d 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -138,7 +138,9 @@ type 'a proof_entry = { let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty -let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types +(** [univsbody] are universe-constraints attached to the body-only, + used in vio-delayed opaque constants and private poly universes *) +let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body = { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff); proof_entry_secctx = section_vars; @@ -148,6 +150,9 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?sect proof_entry_feedback = feedback_id; proof_entry_inline_code = inline} +let definition_entry = + definition_entry_core ?fix_exn:None ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None + type proof_object = { name : Names.Id.t (* [name] only used in the STM *) @@ -173,11 +178,17 @@ let prepare_proof ~unsafe_typ { proof } = let evd = Evd.minimize_universes evd in let to_constr_body c = match EConstr.to_constr_opt evd c with - | Some p -> p - | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") + | Some p -> + Vars.universes_of_constr p, p + | None -> + CErrors.user_err Pp.(str "Some unresolved existential variables remain") in let to_constr_typ t = - if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t + if unsafe_typ + then + let t = EConstr.Unsafe.to_constr t in + Vars.universes_of_constr t, t + else to_constr_body t in (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects @@ -194,6 +205,40 @@ let prepare_proof ~unsafe_typ { proof } = let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in proofs, Evd.evar_universe_context evd +let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl + (used_univs_typ, typ) (used_univs_body, body) = + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let utyp = UState.univ_entry ~poly initial_euctx in + let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in + (* For vi2vo compilation proofs are computed now but we need to + complement the univ constraints of the typ with the ones of + the body. So we keep the two sets distinct. *) + let uctx_body = UState.restrict uctx used_univs in + let ubody = UState.check_mono_univ_decl uctx_body udecl in + utyp, ubody + +let make_univs_private_poly ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) = + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let universes = UState.restrict uctx used_univs in + let typus = UState.restrict universes used_univs_typ in + let utyp = UState.check_univ_decl ~poly typus udecl in + let ubody = Univ.ContextSet.diff + (UState.context_set universes) + (UState.context_set typus) + in + utyp, ubody + +let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) = + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + (* Since the proof is computed now, we can simply have 1 set of + constraints in which we merge the ones for the body and the ones + for the typ. We recheck the declaration after restricting with + the actually used universes. + TODO: check if restrict is really necessary now. *) + let ctx = UState.restrict uctx used_univs in + let utyp = UState.check_univ_decl ~poly ctx udecl in + utyp, Univ.ContextSet.empty + let close_proof ~opaque ~keep_body_ucst_separate ps = let { section_vars; proof; udecl; initial_euctx } = ps in @@ -202,46 +247,19 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = let elist, uctx = prepare_proof ~unsafe_typ ps in let opaque = match opaque with Opaque -> true | Transparent -> false in - let make_entry ((body, eff), typ) = - - let allow_deferred = - not poly && - (keep_body_ucst_separate - || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private)) - in - let used_univs_body = Vars.universes_of_constr body in - let used_univs_typ = Vars.universes_of_constr typ in - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let make_entry ((((_ub, body) as b), eff), ((_ut, typ) as t)) = let utyp, ubody = - if allow_deferred then - let utyp = UState.univ_entry ~poly initial_euctx in - let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in - (* For vi2vo compilation proofs are computed now but we need to - complement the univ constraints of the typ with the ones of - the body. So we keep the two sets distinct. *) - let uctx_body = UState.restrict uctx used_univs in - let ubody = UState.check_mono_univ_decl uctx_body udecl in - utyp, ubody - else if poly && opaque && private_poly_univs () then - let universes = UState.restrict uctx used_univs in - let typus = UState.restrict universes used_univs_typ in - let utyp = UState.check_univ_decl ~poly typus udecl in - let ubody = Univ.ContextSet.diff - (UState.context_set universes) - (UState.context_set typus) - in - utyp, ubody - else - (* Since the proof is computed now, we can simply have 1 set of - constraints in which we merge the ones for the body and the ones - for the typ. We recheck the declaration after restricting with - the actually used universes. - TODO: check if restrict is really necessary now. *) - let ctx = UState.restrict uctx used_univs in - let utyp = UState.check_univ_decl ~poly ctx udecl in - utyp, Univ.ContextSet.empty + (* allow_deferred case *) + if not poly && + (keep_body_ucst_separate + || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private)) + then make_univs_deferred ~initial_euctx ~poly ~uctx ~udecl t b + (* private_poly_univs case *) + else if poly && opaque && private_poly_univs () + then make_univs_private_poly ~poly ~uctx ~udecl t b + else make_univs ~poly ~uctx ~udecl t b in - definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body + definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body in let entries = CList.map make_entry elist in { name; entries; uctx } @@ -734,7 +752,7 @@ let return_partial_proof { proof } = let return_proof ps = let p, uctx = prepare_proof ~unsafe_typ:false ps in - List.map fst p, uctx + List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx let update_global_env = map_proof (fun p -> @@ -889,7 +907,7 @@ module Hook = struct end (* Locality stuff *) -let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = +let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry = let should_suggest = entry.proof_entry_opaque && Option.is_empty entry.proof_entry_secctx in let ubind = UState.universe_binders uctx in @@ -910,6 +928,8 @@ let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; dref +let declare_entry = declare_entry_core ~obls:[] + let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = match possible_indexes with | Some possible_indexes -> @@ -936,7 +956,7 @@ module Recthm = struct } end -let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = +let declare_mutually_recursive_core ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = let vars, fixdecls, indexes = mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in let uctx, univs = @@ -962,6 +982,8 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; csts +let declare_mutually_recursive = declare_mutually_recursive_core ~restrict_ucontext:true + let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ @@ -998,14 +1020,16 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma sigma (fun nf -> nf body, Option.map nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in - let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in + let entry = definition_entry_core ?fix_exn ?opaque ?inline ?types ~univs body in let uctx = Evd.evar_universe_context sigma in entry, uctx -let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook - ?obls ~poly ?inline ~types ~body ?fix_exn sigma = +let declare_definition_core ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook + ~obls ~poly ?inline ~types ~body ?fix_exn sigma = let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in - declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry + declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry + +let declare_definition = declare_definition_core ~obls:[] let prepare_obligation ~name ~types ~body sigma = let env = Global.env () in @@ -1255,8 +1279,8 @@ let not_transp_msg = ++ spc () ++ str "Use 'Defined' instead.") -let pperror cmd = CErrors.user_err ~hdr:"Program" cmd -let err_not_transp () = pperror not_transp_msg +let err_not_transp () = + CErrors.user_err ~hdr:"Program" not_transp_msg module ProgMap = Id.Map @@ -1445,7 +1469,7 @@ let declare_definition prg = let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in (* XXX: This is doing normalization twice *) let kn = - declare_definition ~name ~scope ~kind ~impargs ?hook ~obls + declare_definition_core ~name ~scope ~kind ~impargs ?hook ~obls ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in let pm = progmap_remove !State.prg_ref prg in @@ -1531,7 +1555,7 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let udecl = UState.default_univ_decl in let kns = - declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns + declare_mutually_recursive_core ~scope ~opaque ~kind ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly ~restrict_ucontext:false fixitems in diff --git a/vernac/declare.mli b/vernac/declare.mli index 647896e2f5..5339f4702b 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -144,17 +144,10 @@ val declare_variable for removal from the public API, use higher-level declare APIs instead *) val definition_entry - : ?fix_exn:Future.fix_exn - -> ?opaque:bool + : ?opaque:bool -> ?inline:bool - -> ?feedback_id:Stateid.t - -> ?section_vars:Id.Set.t -> ?types:types -> ?univs:Entries.universes_entry - -> ?eff:Evd.side_effects - -> ?univsbody:Univ.ContextSet.t - (** Universe-constraints attached to the body-only, used in - vio-delayed opaque constants and private poly universes *) -> constr -> Evd.side_effects proof_entry @@ -295,7 +288,6 @@ val declare_entry -> scope:locality -> kind:Decls.logical_kind -> ?hook:Hook.t - -> ?obls:(Id.t * Constr.t) list -> impargs:Impargs.manual_implicits -> uctx:UState.t -> Evd.side_effects proof_entry @@ -315,7 +307,6 @@ val declare_definition -> impargs:Impargs.manual_implicits -> udecl:UState.universe_decl -> ?hook:Hook.t - -> ?obls:(Id.t * Constr.t) list -> poly:bool -> ?inline:bool -> types:EConstr.t option @@ -359,9 +350,6 @@ val declare_mutually_recursive -> ntns:Vernacexpr.decl_notation list -> rec_declaration:Constr.rec_declaration -> possible_indexes:lemma_possible_guards option - -> ?restrict_ucontext:bool - (** XXX: restrict_ucontext should be always true, this seems like a - bug in obligations, so this parameter should go away *) -> Recthm.t list -> Names.GlobRef.t list diff --git a/vernac/mltop.ml b/vernac/mltop.ml index d276a1ac35..c33b3d29f8 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -309,6 +309,9 @@ type ml_module_object = { } let add_module_digest m = + if not has_dynlink then + m, NoDigest + else try let file = file_of_name m in let path, file = System.where_in_path ~warn:false !coq_mlpath_copy file in diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 102a17b216..c21951373b 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -132,5 +132,4 @@ val show_obligations : ?msg:bool -> Names.Id.t option -> unit val show_term : Names.Id.t option -> Pp.t val admit_obligations : Names.Id.t option -> unit -val explain_no_obligations : Names.Id.t option -> Pp.t val check_program_libraries : unit -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 106fed124e..9a1d935928 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1081,10 +1081,9 @@ let vernac_end_segment ({v=id} as lid) = (* Libraries *) let warn_require_in_section = - let name = "require-in-section" in - let category = "deprecated" in - CWarnings.create ~name ~category - (fun () -> strbrk "Use of “Require” inside a section is deprecated.") + CWarnings.create ~name:"require-in-section" ~category:"fragile" + (fun () -> strbrk "Use of “Require” inside a section is fragile." ++ spc() ++ + strbrk "It is not recommended to use this functionality in finished proof scripts.") let vernac_require from import qidl = if Global.sections_are_opened () then warn_require_in_section (); |