From 0c1af31e9d338a13b7df2b4468b81e76ef182d32 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 25 Jun 2020 23:35:20 +0200
Subject: Add a type of format strings to Ltac2.

It provides an abstract type of well-typed format strings, a scope to parse
them and a minimal printf-like API.
---
 doc/stdlib/index-list.html.template | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index cbe526be68..1bc0c1f6d7 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -691,6 +691,7 @@ through the <tt>Require Import</tt> command.</p>
     user-contrib/Ltac2/Notations.v
     user-contrib/Ltac2/Option.v
     user-contrib/Ltac2/Pattern.v
+    user-contrib/Ltac2/Printf.v
     user-contrib/Ltac2/Std.v
     user-contrib/Ltac2/String.v
   </dd>
-- 
cgit v1.2.3


From 14875457711853bcbf7021fba9490e554324a043 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 21 Jan 2021 14:42:29 +0100
Subject: Add documentation for Ltac2 Printf.

---
 doc/changelog/05-tactic-language/13236-ltac2-printf.rst | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 doc/changelog/05-tactic-language/13236-ltac2-printf.rst

(limited to 'doc')

diff --git a/doc/changelog/05-tactic-language/13236-ltac2-printf.rst b/doc/changelog/05-tactic-language/13236-ltac2-printf.rst
new file mode 100644
index 0000000000..02213f22e5
--- /dev/null
+++ b/doc/changelog/05-tactic-language/13236-ltac2-printf.rst
@@ -0,0 +1,7 @@
+- **Added:**
+  Added a ``printf`` macro to Ltac2. It can be made accessible by
+  importing the ``Ltac2.Printf`` module. See the documentation
+  there for more information
+  (`#13236 <https://github.com/coq/coq/pull/13236>`_,
+  fixes `#10108 <https://github.com/coq/coq/issues/10108>`_,
+  by Pierre-Marie Pédrot).
-- 
cgit v1.2.3