Merge PR coq#18095: Extensions to the Ltac2 standard library

Reviewed-by: SkySkimmer Ack-by: Janno Ack-by: JasonGross Ack-by: ppedrot Ack-by: jfehrle Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre · Oct 30, 2023 · f55c63a · f55c63a
1 parent e77d99c
commit f55c63a
Show file tree

Hide file tree

Showing 15 changed files with 516 additions and 127 deletions.
diff --git a/doc/changelog/06-Ltac2-language/18095-br-ltac2-extensions.rst b/doc/changelog/06-Ltac2-language/18095-br-ltac2-extensions.rst
@@ -0,0 +1,8 @@
+- **Added:**
+  new Ltac2 standard library modules `Ltac2.Ref`, `Ltac2.Lazy` and `Ltac2.RedFlags`
+- **Added:**
+  new Ltac2 standard library functions to `Ltac2.Control`, `Ltac2.Array`, and
+  `Ltac2.List`
+  (`#18095 <https://github.com/coq/coq/pull/18095>`_,
+  fixes `#10112 <https://github.com/coq/coq/issues/10112>`_,
+  by Rodolphe Lepigre).
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
@@ -686,6 +686,7 @@ through the <tt>Require Import</tt> command.</p>
     user-contrib/Ltac2/Ind.v
     user-contrib/Ltac2/Init.v
     user-contrib/Ltac2/Int.v
+    user-contrib/Ltac2/Lazy.v
     user-contrib/Ltac2/List.v
     user-contrib/Ltac2/Ltac1.v
     user-contrib/Ltac2/Message.v
@@ -695,6 +696,8 @@ through the <tt>Require Import</tt> command.</p>
     user-contrib/Ltac2/Pattern.v
     user-contrib/Ltac2/Printf.v
     user-contrib/Ltac2/Proj.v
+    user-contrib/Ltac2/RedFlags.v
+    user-contrib/Ltac2/Ref.v
     user-contrib/Ltac2/Std.v
     user-contrib/Ltac2/String.v
     user-contrib/Ltac2/TransparentState.v