From 1b69020c507dc007e5fb9310683ca5568c160be8 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 5 Jun 2019 11:03:00 +0200 Subject: Add codeowner for Ltac2. Forgotten in #10002. Who should be secondary owner? --- .github/CODEOWNERS | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 06a733be45..2a325f2d71 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -173,6 +173,8 @@ azure-pipelines.yml @coq/ci-maintainers /plugins/rtauto/ @PierreCorbineau # Secondary maintainer @herbelin +/user-contrib/Ltac2 @ppedrot + ########## Pretyper ########## /pretyping/ @mattam82 -- cgit v1.2.3 From 3433bcfc128255e35195608eae98b74621eb449e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 5 Jun 2019 11:12:24 +0200 Subject: Changelog entry for Ltac2 (missing from #10002). --- doc/changelog/05-tactic-language/10002-ltac2.rst | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 doc/changelog/05-tactic-language/10002-ltac2.rst diff --git a/doc/changelog/05-tactic-language/10002-ltac2.rst b/doc/changelog/05-tactic-language/10002-ltac2.rst new file mode 100644 index 0000000000..6d62f11eff --- /dev/null +++ b/doc/changelog/05-tactic-language/10002-ltac2.rst @@ -0,0 +1,9 @@ +- Ltac2, a new version of the tactic language Ltac, that doesn't + preserve backward compatibility, has been integrated in the main Coq + distribution. It is still experimental, but we already recommend + users of advanced Ltac to start using it and report bugs or request + enhancements. See its documentation in the :ref:`dedicated chapter + ` (`#10002 `_, plugin + authored by Pierre-Marie Pédrot, with contributions by various + users, integration by Maxime Dénès, help on integrating / improving + the documentation by Théo Zimmermann and Jim Fehrle). -- cgit v1.2.3