diff options
| author | Emilio Jesus Gallego Arias | 2020-01-17 01:25:06 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-01-17 18:02:33 +0100 |
| commit | a47e2f6587e3507a12d4d86b9769b93e01023350 (patch) | |
| tree | 495c3402489dfcfeb78d903a0e5011cf75017b37 /doc/stdlib/index-list.html.template | |
| parent | 55ded80878d47037e49ca9b60f89c422d184899f (diff) | |
[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.
Diffstat (limited to 'doc/stdlib/index-list.html.template')
| -rw-r--r-- | doc/stdlib/index-list.html.template | 25 |
1 files changed, 25 insertions, 0 deletions
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> |