diff options
Diffstat (limited to 'doc/changelog/05-tactic-language')
7 files changed, 0 insertions, 37 deletions
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). |