diff options
Diffstat (limited to 'doc/stdlib')
| -rw-r--r-- | doc/stdlib/dune | 3 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 3 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 4 |
3 files changed, 6 insertions, 4 deletions
diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 0b6ca5f178..6b51202f6e 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -22,7 +22,8 @@ (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) ; For .glob files, should be gone when Coq Dune is smarter. - (package coq)) + (package coq-core) + (package coq-stdlib)) (action (progn (run mkdir -p html) diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index e4f0967794..bca66cc61b 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -58,10 +58,7 @@ theories/micromega/ZifyPow.v theories/micromega/Zify.v theories/nsatz/NsatzTactic.v theories/nsatz/Nsatz.v -theories/omega/Omega.v theories/omega/OmegaLemmas.v -theories/omega/OmegaPlugin.v -theories/omega/OmegaTactic.v theories/omega/PreOmega.v theories/quote/Quote.v theories/romega/ROmega.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index cbe526be68..6fda3b06ce 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -135,6 +135,7 @@ through the <tt>Require Import</tt> command.</p> theories/Arith/Bool_nat.v theories/Arith/Factorial.v theories/Arith/Wf_nat.v + theories/Arith/Cantor.v </dd> <dt> <b>PArith</b>: @@ -286,6 +287,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Cyclic/Int63/Cyclic63.v theories/Numbers/Cyclic/Int63/PrimInt63.v theories/Numbers/Cyclic/Int63/Int63.v + theories/Numbers/Cyclic/Int63/Sint63.v theories/Numbers/Cyclic/Int63/Ring63.v theories/Numbers/Cyclic/ZModulo/ZModulo.v </dd> @@ -684,6 +686,7 @@ through the <tt>Require Import</tt> command.</p> user-contrib/Ltac2/Fresh.v user-contrib/Ltac2/Ident.v user-contrib/Ltac2/Init.v + user-contrib/Ltac2/Ind.v user-contrib/Ltac2/Int.v user-contrib/Ltac2/List.v user-contrib/Ltac2/Ltac1.v @@ -691,6 +694,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> |