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 (limited to 'doc') 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