From a47e2f6587e3507a12d4d86b9769b93e01023350 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 17 Jan 2020 01:25:06 +0100
Subject: [doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]

This partially fixes #10139 ; we now build the Ltac2 documentation and
deploy it.

The fix here can be used for inspiration to do the make-based part.
---
 doc/stdlib/index-list.html.template | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'doc/stdlib/index-list.html.template')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index ac611926b3..5e13214a1a 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -626,6 +626,31 @@ through the <tt>Require Import</tt> command.</p>
     plugins/ssr/ssrfun.v
   </dd>
 
+  <dt> <b>Ltac2</b>:
+    The Ltac2 tactic programming language
+  </dt>
+  <dd>
+    user-contrib/Ltac2/Ltac2.v
+    user-contrib/Ltac2/Array.v
+    user-contrib/Ltac2/Bool.v
+    user-contrib/Ltac2/Char.v
+    user-contrib/Ltac2/Constr.v
+    user-contrib/Ltac2/Control.v
+    user-contrib/Ltac2/Env.v
+    user-contrib/Ltac2/Fresh.v
+    user-contrib/Ltac2/Ident.v
+    user-contrib/Ltac2/Init.v
+    user-contrib/Ltac2/Int.v
+    user-contrib/Ltac2/List.v
+    user-contrib/Ltac2/Ltac1.v
+    user-contrib/Ltac2/Message.v
+    user-contrib/Ltac2/Notations.v
+    user-contrib/Ltac2/Option.v
+    user-contrib/Ltac2/Pattern.v
+    user-contrib/Ltac2/Std.v
+    user-contrib/Ltac2/String.v
+  </dd>
+
   <dt> <b>Unicode</b>:
     Unicode-based notations
   </dt>
-- 
cgit v1.2.3