diff options
| author | Théo Zimmermann | 2020-01-17 19:37:58 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-17 19:37:58 +0100 |
| commit | 1f3ad4f8ebbf48d68488d19335d3c2db18e248f4 (patch) | |
| tree | 349f615d456252c593e4a0512de732c914fa9903 /doc/stdlib/index-list.html.template | |
| parent | 58a9fa018995aa59e30bb7156a6c91b640f88730 (diff) | |
| parent | c3cf1451e6a07a30f58b5704474b19ce7feb1afa (diff) | |
Merge PR #11413: [doc] [ltac2] Build Ltac2 documentation
Reviewed-by: Zimmi48
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> |