diff options
Diffstat (limited to 'doc/stdlib')
| -rw-r--r-- | doc/stdlib/hidden-files | 2 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 67d0b37e81..3af16cb731 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -44,6 +44,7 @@ theories/micromega/Refl.v theories/micromega/RingMicromega.v theories/micromega/Tauto.v theories/micromega/VarMap.v +theories/micromega/ZArith_hints.v theories/micromega/ZCoeff.v theories/micromega/ZMicromega.v theories/micromega/ZifyInst.v @@ -52,6 +53,7 @@ theories/micromega/ZifyComparison.v theories/micromega/ZifyClasses.v theories/micromega/ZifyPow.v theories/micromega/Zify.v +theories/nsatz/NsatzTactic.v theories/nsatz/Nsatz.v theories/omega/Omega.v theories/omega/OmegaLemmas.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index e64b4be454..b2c9c936c9 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -13,6 +13,7 @@ through the <tt>Require Import</tt> command.</p> The core library (automatically loaded when starting Coq) </dt> <dd> + theories/Init/Ltac.v theories/Init/Notations.v theories/Init/Datatypes.v theories/Init/Logic.v @@ -444,6 +445,7 @@ through the <tt>Require Import</tt> command.</p> theories/Sorting/PermutSetoid.v theories/Sorting/Mergesort.v theories/Sorting/Sorted.v + theories/Sorting/CPermutation.v </dd> <dt> <b>Wellfounded</b>: @@ -558,6 +560,7 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/Rtrigo_fun.v theories/Reals/Rtrigo1.v theories/Reals/Rtrigo.v + theories/Reals/Rtrigo_facts.v theories/Reals/Ratan.v theories/Reals/Machin.v theories/Reals/SplitAbsolu.v |