1 files changed, 41 insertions, 12 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index ac611926b3..e64b4be454 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -528,13 +528,17 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Reals/Rdefinitions.v
-    theories/Reals/ConstructiveReals.v
-    theories/Reals/ConstructiveRealsMorphisms.v
-    theories/Reals/ConstructiveCauchyReals.v
-    theories/Reals/ConstructiveCauchyRealsMult.v
+    theories/Reals/Cauchy/ConstructiveCauchyReals.v
+    theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
+    theories/Reals/Cauchy/ConstructiveCauchyAbs.v
     theories/Reals/ClassicalDedekindReals.v
     theories/Reals/Raxioms.v
-    theories/Reals/ConstructiveRealsLUB.v
+    theories/Reals/Abstract/ConstructiveReals.v
+    theories/Reals/Abstract/ConstructiveRealsMorphisms.v
+    theories/Reals/Abstract/ConstructiveLUB.v
+    theories/Reals/Abstract/ConstructiveAbs.v
+    theories/Reals/Abstract/ConstructiveLimits.v
+    theories/Reals/Abstract/ConstructiveSum.v
     theories/Reals/RIneq.v
     theories/Reals/DiscrR.v
     theories/Reals/ROrderedType.v
@@ -579,7 +583,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/Ranalysis5.v
     theories/Reals/Ranalysis_reg.v
     theories/Reals/Rcomplete.v
-    theories/Reals/ConstructiveRcomplete.v
+    theories/Reals/Cauchy/ConstructiveRcomplete.v
     theories/Reals/RiemannInt.v
     theories/Reals/RiemannInt_SF.v
     theories/Reals/Rpow_def.v
@@ -595,6 +599,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/SeqSeries.v
     theories/Reals/Sqrt_reg.v
     theories/Reals/Rlogic.v
+    theories/Reals/Rregisternames.v
     (theories/Reals/Reals.v)
     theories/Reals/Runcountable.v
   </dd>
@@ -619,11 +624,36 @@ through the <tt>Require Import</tt> command.</p>
     small scale reflection formalization technique
   </dt>
   <dd>
-    plugins/ssrmatching/ssrmatching.v
-    plugins/ssr/ssrclasses.v
-    plugins/ssr/ssreflect.v
-    plugins/ssr/ssrbool.v
-    plugins/ssr/ssrfun.v
+    theories/ssrmatching/ssrmatching.v
+    theories/ssr/ssrclasses.v
+    theories/ssr/ssreflect.v
+    theories/ssr/ssrbool.v
+    theories/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>:
@@ -639,7 +669,6 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq89.v
     theories/Compat/Coq810.v
     theories/Compat/Coq811.v
     theories/Compat/Coq812.v