Release notes for 8.12.

20 files changed, 0 insertions, 140 deletions

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).