aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/05-tactic-language
AgeCommit message (Expand)Author
2021-04-22Merge PR #14128: Uniformize the name of the Ltac2 boolean equality function.coqbot-app[bot]
2021-04-17Uniformize the name of the Ltac2 boolean equality function.Pierre-Marie Pédrot
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
2021-03-29Added a changelog.Pierre-Marie Pédrot
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat...Michael Soegtrop
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
2021-03-16Adding a changelog and registering the new file in the documentation.Pierre-Marie Pédrot
2021-03-13Documenting the changes.Pierre-Marie Pédrot
2021-03-10Add documentation.Pierre-Marie Pédrot
2021-03-10Adding documentation of the changes.Pierre-Marie Pédrot
2021-01-22Add documentation for Ltac2 Printf.Pierre-Marie Pédrot
2020-12-04Merge PR #13442: Add an abstraction function in the LtacX FFI.coqbot-app[bot]
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-11-30Adding a changelog for Ltac1.lambda.Pierre-Marie Pédrot
2020-11-05Changelog for 8.12.1.Théo Zimmermann
2020-11-04Document the syntax addition.Pierre-Marie Pédrot
2020-10-28Adding changelog for #13247.Hugo Herbelin
2020-09-22Adding change log for #13028.Hugo Herbelin
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-01Add a changelog.Pierre-Marie Pédrot
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
2020-05-12Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.Jason Gross
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.Pierre-Marie Pédrot
2020-05-08In non-strict mode, accept any variable as a tactic reference.Pierre-Marie Pédrot
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
2020-04-03Adding change log.Hugo Herbelin
2020-03-08Minor improvements to the unreleased changelog.Théo Zimmermann
2020-03-03Ltac2: Add notation for enough and eenoughMichael Soegtrop
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
2020-01-22Changelog for 8.11.0.Théo Zimmermann
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-11-28[changelog] Add types to changelog entries.Théo Zimmermann
2019-10-24Release notes for Coq 8.10.1Vincent Laporte
2019-10-21Adding changelogHugo Herbelin
2019-07-29Document changes by PR 10324Vincent Laporte
2019-06-08Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ...Pierre-Marie Pédrot
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-05Changelog entry for Ltac2 (missing from #10002).Théo Zimmermann
2019-05-05Create categories in changelog.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:48:03 +0000