From befc5606d619ee1e377d2fb21d13909fbd077d72 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Mon, 20 Jan 2025 17:12:37 +0100
Subject: [PATCH 1/3] Header and footer for new website (rocq-prover.org)
 integration

---
 doc/common/styles/html/coqremote/footer.html | 445 ++++++++++++++++++-
 doc/common/styles/html/coqremote/header.html | 303 +++++++++++--
 2 files changed, 690 insertions(+), 58 deletions(-)

diff --git a/doc/common/styles/html/coqremote/footer.html b/doc/common/styles/html/coqremote/footer.html
index 23dfccb62c..710f8d0983 100644
--- a/doc/common/styles/html/coqremote/footer.html
+++ b/doc/common/styles/html/coqremote/footer.html
@@ -1,34 +1,431 @@
-    <div id="sidebarWrapper">
-      <div id="sidebar">
-        <div class="block">
-          <h2 class="title">Navigation</h2>
-          <div class="content">
-            <ul class="menu">
-              <li class="leaf">Standard Library
-                <ul class="menu">
-                  <li><a href="index.html">Table of contents</a></li>
-                  <li><a href="genindex.html">Index</a></li>
-                </ul>
-              </li>
-            </ul>
+
+          <!-- ************************
+            START STDLIB FOOTER 
+          ************************* -->
           </div>
         </div>
       </div>
     </div>
 
-  </div>
+  </main>
+
+
+
+  <button class="fixed bottom-8 right-10 md:bottom-[5rem] lg:bottom-[8.37rem] lg:right-[6.5rem] border-0 hidden focus:outline-none z-50 rounded-full shadow-custom p-4 bg-primary dark:bg-dark-primary" onclick="scrollToTop()" id="scrollToTop" title="Scroll to top" style="display: block;"><svg class="h-6 w-6" viewBox="0 0 24 24" fill="currentColor" xmlns="http://www.w3.org/2000/svg">
+      <path d="M4.5 10.5L12 3M12 3L19.5 10.5M12 3V21" stroke="white" stroke-width="1.5" stroke-linecap="round" stroke-linejoin="round"></path>
+    </svg>
+
+  </button>
+
+  <footer x-data="" class="border-t border-separator_30 dark:border-dark-separator_30 bg-dark-sand dark:bg-dark-card" aria-labelledby="footer-heading">
+    <h2 id="footer-heading" class="sr-only">Footer</h2>
+    <div class="mx-auto max-w-7xl px-6 py-16 lg:px-8">
+      <div class="flex w-full items-center justify-between mb-8">
+        <a href="http://rocq-prover.org/"><img class="h-8 dark:hidden" src="https://rocq-prover.org/logos/logo-rocq-blue_orange.svg" alt="Rocq">
+          <img class="h-8 hidden dark:inline" src="https://rocq-prover.org/logos/logo-rocq-white.svg" alt="Rocq">
+        </a>
+        <div class="hidden md:flex">
+          <button class="flex grow basis-0 justify-center items-center py-2 px-4 text-sm border rounded-l rounded-l-full border-r-0 bg-gradient-to-r from-[#FF540A] to-[#FF7033] border-gray-200 dark:border-gray-300 text-white dark:text-dark-title " :class="$store.themeSettings.preference === &quot;light&quot; ? &quot;bg-gradient-to-r from-[#FF540A] to-[#FF7033] border-gray-200 dark:border-gray-300 text-white dark:text-dark-title &quot; : &quot;bg-white text-content outline-2 outline-card_border dark:outline-dark-separator_30&quot;" @click="$store.themeSettings.setPreference(&quot;light&quot;)">
+            <svg xmlns="http://www.w3.org/2000/svg" width="14" height="14" viewBox="0 0 14 14" fill="none" class="mr-2">
+              <path d="M7 0.5V2.125M11.5962 2.40378L10.4472 3.55283M13.5 7H11.875M11.5962 11.5962L10.4472 10.4472M7 11.875V13.5M3.55283 10.4472L2.40378 11.5962M2.125 7H0.5M3.55283 3.55283L2.40378 2.40378M9.70833 7C9.70833 7.71829 9.42299 8.40717 8.91508 8.91508C8.40717 9.42299 7.71829 9.70833 7 9.70833C6.28171 9.70833 5.59283 9.42299 5.08492 8.91508C4.57701 8.40717 4.29167 7.71829 4.29167 7C4.29167 6.28171 4.57701 5.59283 5.08492 5.08492C5.59283 4.57701 6.28171 4.29167 7 4.29167C7.71829 4.29167 8.40717 4.57701 8.91508 5.08492C9.42299 5.59283 9.70833 6.28171 9.70833 7Z" stroke="currentColor" stroke-linecap="round" stroke-linejoin="round"></path>
+            </svg>
+
+
+            Light
+          </button>
+
+
+          <button class="flex grow basis-0 justify-center items-center py-2 px-4 text-sm border border-r-0 bg-white text-content outline-2 outline-card_border dark:outline-dark-separator_30" :class="$store.themeSettings.preference === &quot;dark&quot; ? &quot;bg-gradient-to-r from-[#260085] to-[#170052] border-gray-200 dark:border-gray-300 text-white dark:text-dark-title &quot; : &quot;bg-white text-content outline-2 outline-card_border dark:outline-dark-separator_30&quot;" @click="$store.themeSettings.setPreference(&quot;dark&quot;)">
+            <svg xmlns="http://www.w3.org/2000/svg" width="12" height="12" viewBox="0 0 12 12" fill="none" class="mr-2">
+              <path d="M11.1573 7.90842C10.5134 8.17678 9.8226 8.3145 9.125 8.31358C6.20812 8.31358 3.84375 5.94921 3.84375 3.03233C3.84375 2.31192 3.98783 1.62562 4.24892 1C3.28663 1.40144 2.46465 2.07865 1.88651 2.94635C1.30836 3.81404 0.999911 4.83342 1 5.87608C1 8.79296 3.36437 11.1573 6.28125 11.1573C7.32391 11.1574 8.34329 10.849 9.21099 10.2708C10.0787 9.69268 10.7559 8.8707 11.1573 7.90842Z" stroke="currentColor" stroke-linecap="round" stroke-linejoin="round"></path>
+            </svg>
+
+
+            Dark
+          </button>
+
+
+          <button class="flex grow basis-0 justify-center items-center py-2 px-4 text-sm border rounded-r rounded-r-full bg-white text-content outline-2 outline-card_border dark:outline-dark-separator_30" :class="$store.themeSettings.preference === &quot;system&quot; ? &quot;bg-gradient-to-r from-[#2B7866] to-[#004039] border-gray-200 dark:border-gray-300 text-white dark:text-dark-title &quot; : &quot;bg-white text-content outline-2 outline-card_border dark:outline-dark-separator_30&quot;" @click="$store.themeSettings.setPreference(&quot;system&quot;)">
+            <svg xmlns="http://www.w3.org/2000/svg" width="18" height="18" viewBox="0 0 18 18" fill="none" class="mr-2">
+              <path d="M7.19553 2.955C7.26303 2.5485 7.61553 2.25 8.02803 2.25H9.97278C10.3853 2.25 10.7378 2.5485 10.8053 2.955L10.965 3.91575C11.0123 4.19625 11.1998 4.43025 11.4488 4.56825C11.5043 4.59825 11.559 4.6305 11.6138 4.6635C11.8575 4.8105 12.1538 4.85625 12.42 4.7565L13.3328 4.4145C13.5198 4.34416 13.7258 4.34248 13.9139 4.40978C14.1021 4.47708 14.2603 4.60899 14.3603 4.782L15.3323 6.46725C15.4321 6.64028 15.4672 6.8431 15.4315 7.03962C15.3958 7.23615 15.2916 7.41363 15.1373 7.5405L14.385 8.16075C14.1653 8.3415 14.0565 8.6205 14.0625 8.90475C14.0636 8.9685 14.0636 9.03225 14.0625 9.096C14.0565 9.3795 14.1653 9.6585 14.385 9.83925L15.138 10.4595C15.456 10.722 15.5385 11.1758 15.333 11.532L14.3595 13.2172C14.2597 13.3902 14.1017 13.5222 13.9137 13.5896C13.7257 13.657 13.5198 13.6556 13.3328 13.5855L12.42 13.2435C12.1538 13.1438 11.8575 13.1895 11.613 13.3365C11.5587 13.3696 11.5037 13.4016 11.448 13.4325C11.1998 13.5697 11.0123 13.8037 10.965 14.0842L10.8053 15.045C10.7378 15.4523 10.3853 15.75 9.97278 15.75H8.02728C7.61478 15.75 7.26303 15.4515 7.19478 15.045L7.03503 14.0842C6.98853 13.8037 6.80103 13.5698 6.55203 13.4318C6.49642 13.4011 6.44141 13.3693 6.38703 13.3365C6.14328 13.1895 5.84703 13.1438 5.58003 13.2435L4.66728 13.5855C4.48033 13.6556 4.27456 13.6572 4.08656 13.5899C3.89856 13.5226 3.74051 13.3908 3.64053 13.218L2.66778 11.5328C2.56799 11.3597 2.53282 11.1569 2.56852 10.9604C2.60423 10.7639 2.7085 10.5864 2.86278 10.4595L3.61578 9.83925C3.83478 9.65925 3.94353 9.3795 3.93828 9.096C3.93711 9.03226 3.93711 8.96849 3.93828 8.90475C3.94353 8.61975 3.83478 8.3415 3.61578 8.16075L2.86278 7.5405C2.70869 7.41367 2.60454 7.23633 2.56884 7.03997C2.53314 6.84361 2.56819 6.64095 2.66778 6.468L3.64053 4.78275C3.74042 4.6096 3.89854 4.47754 4.08672 4.4101C4.27489 4.34266 4.4809 4.34422 4.66803 4.4145L5.58003 4.7565C5.84703 4.85625 6.14328 4.8105 6.38703 4.6635C6.44103 4.6305 6.49653 4.599 6.55203 4.5675C6.80103 4.43025 6.98853 4.19625 7.03503 3.91575L7.19553 2.955Z" stroke="currentColor" stroke-linecap="round" stroke-linejoin="round"></path>
+              <path d="M11.25 9C11.25 9.59674 11.0129 10.169 10.591 10.591C10.169 11.0129 9.59674 11.25 9 11.25C8.40326 11.25 7.83097 11.0129 7.40901 10.591C6.98705 10.169 6.75 9.59674 6.75 9C6.75 8.40326 6.98705 7.83097 7.40901 7.40901C7.83097 6.98705 8.40326 6.75 9 6.75C9.59674 6.75 10.169 6.98705 10.591 7.40901C11.0129 7.83097 11.25 8.40326 11.25 9Z" stroke="currentColor" stroke-linecap="round" stroke-linejoin="round"></path>
+            </svg>
+
+
+            System
+          </button>
+
+
+
+        </div>
+      </div>
+      <div class="xl:grid xl:grid-cols-3 xl:gap-8">
+        <div class="space-y-8">
+          <p class="text-base leading-6 text-title dark:text-dark-content">Interactive Theorem Prover</p>
+          <div class="flex space-x-6">
+
+            <a href="https://coq.zulipchat.com/" class="text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
+              <span class="sr-only">Zulip</span>
+              <svg viewBox="0 0 256 256" version="1.1" class="h-6 w-6" fill="currentColor" aria-hidden="true" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" preserveAspectRatio="xMidYMid">
+                <path d="M128,0 C198.692448,0 256,57.307552 256,128 C256,198.692448 198.692448,256 128,256 C57.307552,256 0,198.692448 0,128 C0,57.307552 57.307552,0 128,0 Z M121.679533,118.222163 L75.7877336,159.200897 C71.0603547,162.920702 67.9584879,169.060511 67.9584879,175.967416 C67.9584879,187.245548 76.232162,196.475047 86.3444303,196.475047 L172.590938,196.475047 C182.703207,196.475047 190.976881,187.245548 190.976881,175.967416 C190.976881,164.68624 182.703207,155.459784 172.590938,155.459784 L107.299534,155.459784 C106.331533,155.459784 105.719683,154.300009 106.191507,153.356359 L123.024994,119.652857 C123.639888,118.669635 122.531861,117.491595 121.679533,118.222163 Z M172.590938,59.3627915 L86.3444303,59.3627915 C76.232162,59.3627915 67.9584879,68.58925 67.9584879,79.870426 C67.9584879,91.1485579 76.232162,100.378058 86.3444303,100.378058 L86.3444303,100.378058 L151.635834,100.378058 C152.603836,100.378058 153.215686,101.537833 152.743861,102.481482 L152.743861,102.481482 L135.910374,136.184985 C135.29548,137.168207 136.403507,138.346246 137.255836,137.615679 L137.255836,137.615679 L183.147635,96.6308563 C187.875014,92.9080074 190.976881,86.7712425 190.976881,79.8643379 C190.976881,68.586206 182.703207,59.3567064 172.590938,59.3627915 L172.590938,59.3627915 Z" fill="inherit"></path>
+              </svg>
+
+
+            </a>
+
+
+            <a href="https://github.com/rocq-prover" class="text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
+              <span class="sr-only">GitHub</span>
+              <svg xmlns="http://www.w3.org/2000/svg" class="h-6 w-6" fill="currentColor" viewBox="0 0 24 24" aria-hidden="true">
+                <path fill-rule="evenodd" d="M12 2C6.477 2 2 6.484 2 12.017c0 4.425 2.865 8.18 6.839 9.504.5.092.682-.217.682-.483 0-.237-.008-.868-.013-1.703-2.782.605-3.369-1.343-3.369-1.343-.454-1.158-1.11-1.466-1.11-1.466-.908-.62.069-.608.069-.608 1.003.07 1.531 1.032 1.531 1.032.892 1.53 2.341 1.088 2.91.832.092-.647.35-1.088.636-1.338-2.22-.253-4.555-1.113-4.555-4.951 0-1.093.39-1.988 1.029-2.688-.103-.253-.446-1.272.098-2.65 0 0 .84-.27 2.75 1.026A9.564 9.564 0 0112 6.844c.85.004 1.705.115 2.504.337 1.909-1.296 2.747-1.027 2.747-1.027.546 1.379.202 2.398.1 2.651.64.7 1.028 1.595 1.028 2.688 0 3.848-2.339 4.695-4.566 4.943.359.309.678.92.678 1.855 0 1.338-.012 2.419-.012 2.747 0 .268.18.58.688.482A10.019 10.019 0 0022 12.017C22 6.484 17.522 2 12 2z" clip-rule="evenodd"></path>
+              </svg>
+
+
+            </a>
+
+
+            <a href="https://coq.discourse.group/" class="text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
+              <span class="sr-only">Discourse</span>
+              <svg xmlns="http://www.w3.org/2000/svg" class="h-6 w-6" fill="currentColor" viewBox="0 0 448 512" aria-hidden="true">
+                <path d="M225.9 32C103.3 32 0 130.5 0 252.1 0 256 .1 480 .1 480l225.8-.2c122.7 0 222.1-102.3 222.1-223.9C448 134.3 348.6 32 225.9 32zM224 384c-19.4 0-37.9-4.3-54.4-12.1L88.5 392l22.9-75c-9.8-18.1-15.4-38.9-15.4-61 0-70.7 57.3-128 128-128s128 57.3 128 128-57.3 128-128 128z"></path>
+              </svg>
+
+
+
+            </a>
+
+
+            <a href="https://mastodon.acm.org/@RocqProver" class="text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
+              <span class="sr-only">Mastodon</span>
+              <svg viewBox="0 0 74 79" class="h-6 w-6" fill="currentColor" xmlns="http://www.w3.org/2000/svg" aria-hidden="true">
+                <path d="M73.7014 17.4323C72.5616 9.05152 65.1774 2.4469 56.424 1.1671C54.9472 0.950843 49.3518 0.163818 36.3901 0.163818H36.2933C23.3281 0.163818 20.5465 0.950843 19.0697 1.1671C10.56 2.41145 2.78877 8.34604 0.903306 16.826C-0.00357854 21.0022 -0.100361 25.6322 0.068112 29.8793C0.308275 35.9699 0.354874 42.0498 0.91406 48.1156C1.30064 52.1448 1.97502 56.1419 2.93215 60.0769C4.72441 67.3445 11.9795 73.3925 19.0876 75.86C26.6979 78.4332 34.8821 78.8603 42.724 77.0937C43.5866 76.8952 44.4398 76.6647 45.2833 76.4024C47.1867 75.8033 49.4199 75.1332 51.0616 73.9562C51.0841 73.9397 51.1026 73.9184 51.1156 73.8938C51.1286 73.8693 51.1359 73.8421 51.1368 73.8144V67.9366C51.1364 67.9107 51.1302 67.8852 51.1186 67.862C51.1069 67.8388 51.0902 67.8184 51.0695 67.8025C51.0489 67.7865 51.0249 67.7753 50.9994 67.7696C50.9738 67.764 50.9473 67.7641 50.9218 67.7699C45.8976 68.9569 40.7491 69.5519 35.5836 69.5425C26.694 69.5425 24.3031 65.3699 23.6184 63.6327C23.0681 62.1314 22.7186 60.5654 22.5789 58.9744C22.5775 58.9477 22.5825 58.921 22.5934 58.8965C22.6043 58.8721 22.621 58.8505 22.6419 58.8336C22.6629 58.8167 22.6876 58.8049 22.714 58.7992C22.7404 58.7934 22.7678 58.794 22.794 58.8007C27.7345 59.9796 32.799 60.5746 37.8813 60.5733C39.1036 60.5733 40.3223 60.5733 41.5447 60.5414C46.6562 60.3996 52.0437 60.1408 57.0728 59.1694C57.1983 59.1446 57.3237 59.1233 57.4313 59.0914C65.3638 57.5847 72.9128 52.8555 73.6799 40.8799C73.7086 40.4084 73.7803 35.9415 73.7803 35.4523C73.7839 33.7896 74.3216 23.6576 73.7014 17.4323ZM61.4925 47.3144H53.1514V27.107C53.1514 22.8528 51.3591 20.6832 47.7136 20.6832C43.7061 20.6832 41.6988 23.2499 41.6988 28.3194V39.3803H33.4078V28.3194C33.4078 23.2499 31.3969 20.6832 27.3894 20.6832C23.7654 20.6832 21.9552 22.8528 21.9516 27.107V47.3144H13.6176V26.4937C13.6176 22.2395 14.7157 18.8598 16.9118 16.3545C19.1772 13.8552 22.1488 12.5719 25.8373 12.5719C30.1064 12.5719 33.3325 14.1955 35.4832 17.4394L37.5587 20.8853L39.6377 17.4394C41.7884 14.1955 45.0145 12.5719 49.2765 12.5719C52.9614 12.5719 55.9329 13.8552 58.2055 16.3545C60.4017 18.8574 61.4997 22.2371 61.4997 26.4937L61.4925 47.3144Z" fill="inherit"></path>
+              </svg>
+
+
+            </a>
+
+
+            <a href="http://rocq-prover.org/planet.xml" class="text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
+              <span class="sr-only">RSS</span>
+              <svg xmlns="http://www.w3.org/2000/svg" class="h-6 w-6" fill="currentColor" viewBox="0 0 24 24" aria-hidden="true">
+                <path fill-rule="evenodd" d="M15.2692 22H11.3846C11.3846 16.8462 7.11538 12.6154 2 12.6154V8.73077C9.26923 8.73077 15.2692 14.7308 15.2692 22ZM18 22C18 13.2308 10.7692 6 2 6V2C12.9615 2 22 11.0385 22 22H18Z" clip-rule="evenodd"></path>
+                <path fill-rule="evenodd" d="M4.73077 22C6.23893 22 7.46154 20.7774 7.46154 19.2692C7.46154 17.7611 6.23893 16.5385 4.73077 16.5385C3.22261 16.5385 2 17.7611 2 19.2692C2 20.7774 3.22261 22 4.73077 22Z" clip-rule="evenodd"></path>
+              </svg>
+
+
+            </a>
+
+
+          </div>
+          <div class="flex w-full md:hidden">
+            <button class="flex grow basis-0 justify-center items-center py-2 px-4 text-sm border rounded-l rounded-l-full border-r-0 bg-gradient-to-r from-[#FF540A] to-[#FF7033] border-gray-200 dark:border-gray-300 text-white dark:text-dark-title " :class="$store.themeSettings.preference === &quot;light&quot; ? &quot;bg-gradient-to-r from-[#FF540A] to-[#FF7033] border-gray-200 dark:border-gray-300 text-white dark:text-dark-title &quot; : &quot;bg-white text-content outline-2 outline-card_border dark:outline-dark-separator_30&quot;" @click="$store.themeSettings.setPreference(&quot;light&quot;)">
+              <svg xmlns="http://www.w3.org/2000/svg" width="14" height="14" viewBox="0 0 14 14" fill="none" class="mr-2">
+                <path d="M7 0.5V2.125M11.5962 2.40378L10.4472 3.55283M13.5 7H11.875M11.5962 11.5962L10.4472 10.4472M7 11.875V13.5M3.55283 10.4472L2.40378 11.5962M2.125 7H0.5M3.55283 3.55283L2.40378 2.40378M9.70833 7C9.70833 7.71829 9.42299 8.40717 8.91508 8.91508C8.40717 9.42299 7.71829 9.70833 7 9.70833C6.28171 9.70833 5.59283 9.42299 5.08492 8.91508C4.57701 8.40717 4.29167 7.71829 4.29167 7C4.29167 6.28171 4.57701 5.59283 5.08492 5.08492C5.59283 4.57701 6.28171 4.29167 7 4.29167C7.71829 4.29167 8.40717 4.57701 8.91508 5.08492C9.42299 5.59283 9.70833 6.28171 9.70833 7Z" stroke="currentColor" stroke-linecap="round" stroke-linejoin="round"></path>
+              </svg>
+
+
+              Light
+            </button>
+
+
+            <button class="flex grow basis-0 justify-center items-center py-2 px-4 text-sm border border-r-0 bg-white text-content outline-2 outline-card_border dark:outline-dark-separator_30" :class="$store.themeSettings.preference === &quot;dark&quot; ? &quot;bg-gradient-to-r from-[#260085] to-[#170052] border-gray-200 dark:border-gray-300 text-white dark:text-dark-title &quot; : &quot;bg-white text-content outline-2 outline-card_border dark:outline-dark-separator_30&quot;" @click="$store.themeSettings.setPreference(&quot;dark&quot;)">
+              <svg xmlns="http://www.w3.org/2000/svg" width="12" height="12" viewBox="0 0 12 12" fill="none" class="mr-2">
+                <path d="M11.1573 7.90842C10.5134 8.17678 9.8226 8.3145 9.125 8.31358C6.20812 8.31358 3.84375 5.94921 3.84375 3.03233C3.84375 2.31192 3.98783 1.62562 4.24892 1C3.28663 1.40144 2.46465 2.07865 1.88651 2.94635C1.30836 3.81404 0.999911 4.83342 1 5.87608C1 8.79296 3.36437 11.1573 6.28125 11.1573C7.32391 11.1574 8.34329 10.849 9.21099 10.2708C10.0787 9.69268 10.7559 8.8707 11.1573 7.90842Z" stroke="currentColor" stroke-linecap="round" stroke-linejoin="round"></path>
+              </svg>
+
+
+              Dark
+            </button>
+
+
+            <button class="flex grow basis-0 justify-center items-center py-2 px-4 text-sm border rounded-r rounded-r-full bg-white text-content outline-2 outline-card_border dark:outline-dark-separator_30" :class="$store.themeSettings.preference === &quot;system&quot; ? &quot;bg-gradient-to-r from-[#2B7866] to-[#004039] border-gray-200 dark:border-gray-300 text-white dark:text-dark-title &quot; : &quot;bg-white text-content outline-2 outline-card_border dark:outline-dark-separator_30&quot;" @click="$store.themeSettings.setPreference(&quot;system&quot;)">
+              <svg xmlns="http://www.w3.org/2000/svg" width="18" height="18" viewBox="0 0 18 18" fill="none" class="mr-2">
+                <path d="M7.19553 2.955C7.26303 2.5485 7.61553 2.25 8.02803 2.25H9.97278C10.3853 2.25 10.7378 2.5485 10.8053 2.955L10.965 3.91575C11.0123 4.19625 11.1998 4.43025 11.4488 4.56825C11.5043 4.59825 11.559 4.6305 11.6138 4.6635C11.8575 4.8105 12.1538 4.85625 12.42 4.7565L13.3328 4.4145C13.5198 4.34416 13.7258 4.34248 13.9139 4.40978C14.1021 4.47708 14.2603 4.60899 14.3603 4.782L15.3323 6.46725C15.4321 6.64028 15.4672 6.8431 15.4315 7.03962C15.3958 7.23615 15.2916 7.41363 15.1373 7.5405L14.385 8.16075C14.1653 8.3415 14.0565 8.6205 14.0625 8.90475C14.0636 8.9685 14.0636 9.03225 14.0625 9.096C14.0565 9.3795 14.1653 9.6585 14.385 9.83925L15.138 10.4595C15.456 10.722 15.5385 11.1758 15.333 11.532L14.3595 13.2172C14.2597 13.3902 14.1017 13.5222 13.9137 13.5896C13.7257 13.657 13.5198 13.6556 13.3328 13.5855L12.42 13.2435C12.1538 13.1438 11.8575 13.1895 11.613 13.3365C11.5587 13.3696 11.5037 13.4016 11.448 13.4325C11.1998 13.5697 11.0123 13.8037 10.965 14.0842L10.8053 15.045C10.7378 15.4523 10.3853 15.75 9.97278 15.75H8.02728C7.61478 15.75 7.26303 15.4515 7.19478 15.045L7.03503 14.0842C6.98853 13.8037 6.80103 13.5698 6.55203 13.4318C6.49642 13.4011 6.44141 13.3693 6.38703 13.3365C6.14328 13.1895 5.84703 13.1438 5.58003 13.2435L4.66728 13.5855C4.48033 13.6556 4.27456 13.6572 4.08656 13.5899C3.89856 13.5226 3.74051 13.3908 3.64053 13.218L2.66778 11.5328C2.56799 11.3597 2.53282 11.1569 2.56852 10.9604C2.60423 10.7639 2.7085 10.5864 2.86278 10.4595L3.61578 9.83925C3.83478 9.65925 3.94353 9.3795 3.93828 9.096C3.93711 9.03226 3.93711 8.96849 3.93828 8.90475C3.94353 8.61975 3.83478 8.3415 3.61578 8.16075L2.86278 7.5405C2.70869 7.41367 2.60454 7.23633 2.56884 7.03997C2.53314 6.84361 2.56819 6.64095 2.66778 6.468L3.64053 4.78275C3.74042 4.6096 3.89854 4.47754 4.08672 4.4101C4.27489 4.34266 4.4809 4.34422 4.66803 4.4145L5.58003 4.7565C5.84703 4.85625 6.14328 4.8105 6.38703 4.6635C6.44103 4.6305 6.49653 4.599 6.55203 4.5675C6.80103 4.43025 6.98853 4.19625 7.03503 3.91575L7.19553 2.955Z" stroke="currentColor" stroke-linecap="round" stroke-linejoin="round"></path>
+                <path d="M11.25 9C11.25 9.59674 11.0129 10.169 10.591 10.591C10.169 11.0129 9.59674 11.25 9 11.25C8.40326 11.25 7.83097 11.0129 7.40901 10.591C6.98705 10.169 6.75 9.59674 6.75 9C6.75 8.40326 6.98705 7.83097 7.40901 7.40901C7.83097 6.98705 8.40326 6.75 9 6.75C9.59674 6.75 10.169 6.98705 10.591 7.40901C11.0129 7.83097 11.25 8.40326 11.25 9Z" stroke="currentColor" stroke-linecap="round" stroke-linejoin="round"></path>
+              </svg>
+
+
+              System
+            </button>
+
+
+
+          </div>
+          <div class="flex mt-6 space-y-4 hidden">
+
+            <div class="text-base leading-6 text-content dark:text-dark-title">
+              GitHub <a href="https://github.com/coq/rocq-prover.org/tree/main" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">branch</a>
+              and <a href="https://github.com/coq/rocq-prover.org/commit/ab51b997fd3397cb55a9495b3796f804bb15be53">commit</a>.
+            </div>
+
+          </div>
+        </div>
+        <div class="mt-8 grid grid-cols-2 gap-8 xl:col-span-2 xl:mt-0">
+          <div class="md:grid md:grid-cols-2 md:gap-8">
+            <div>
+              <h3 class="text-base font-semibold leading-6 text-title dark:text-dark-content">About Rocq</h3>
+              <ul class="mt-6 space-y-4">
+
+                <li>
+                  <a href="http://rocq-prover.org/changelog" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Changelog</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/releases" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Releases</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/industrial-users" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Industrial Users</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/academic-users" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Academic Users</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/about#history" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">History</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/why" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Why Rocq?</a>
+
+                </li>
+
 
-  <div id="footer">
-    <div id="nav-footer">
-      <ul class="links-menu-footer">
-        <li><a href="mailto:coq-www_@_inria.fr">webmaster</a></li>
-        <li><a href="http://validator.w3.org/">xhtml valid</a></li>
-        <li><a href="http://jigsaw.w3.org/css-validator/">CSS valid</a></li>
-      </ul>
+                <li>
+                  <a href="http://rocq-prover.org/roadmap" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Roadmap</a>
+
+                </li>
+
+
+              </ul>
+            </div>
+            <div class="mt-10 md:mt-0">
+              <h3 class="text-base font-semibold leading-6 text-title dark:text-dark-content">Resources</h3>
+              <ul class="mt-6 space-y-4">
+
+                <li>
+                  <a href="http://rocq-prover.org/install" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Install Rocq</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/docs#beginner_section" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Get Started</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/docs/platform-docs" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Documentation</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/refman" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Reference Manual</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/stdlib" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Standard Library</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/books" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Books</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/exercises" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Exercises</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/papers" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Papers</a>
+
+                </li>
+
+
+                <li>
+                  <a href="https://x80.org/rhino-down/" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Rocq Playground</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/logo" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Logo</a>
+
+                </li>
+
+
+              </ul>
+            </div>
+          </div>
+          <div class="md:grid md:grid-cols-2 md:gap-8">
+            <div>
+              <h3 class="text-base font-semibold leading-6 text-title dark:text-dark-content">Ecosystem</h3>
+              <ul class="mt-6 space-y-4">
+
+                <li>
+                  <a href="http://rocq-prover.org/platform" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Platform</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/packages" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Packages</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/community" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Community</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/consortium" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Consortium</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/events" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Events</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/rocq-planet" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Rocq Planet</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/jobs" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Jobs</a>
+
+                </li>
+
+
+              </ul>
+            </div>
+            <div class="mt-20 md:mt-0">
+              <h3 class="text-base font-semibold leading-6 text-title dark:text-dark-content">Policies</h3>
+              <ul class="mt-6 space-y-4">
+
+                <li>
+                  <a href="http://rocq-prover.org/governance" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Rocq Team</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/policies/governance" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Governance</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/policies/privacy-policy" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Privacy</a>
+
+                </li>
+
+
+                <li>
+                  <a href="http://rocq-prover.org/policies/code-of-conduct" class="text-base leading-6 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">Code of Conduct</a>
+
+                </li>
+
+
+              </ul>
+            </div>
+          </div>
+        </div>
+      </div>
     </div>
-  </div>
+    <script>
+      document.addEventListener('alpine:init', () => {
+        Alpine.store('themeSettings', {
+          init() {
+            this.storageAccess = localStorage.getItem('storageAccess')
+            this.preference = localStorage.getItem('theme') || "system"
+            this.isSystemDefaultDark = window.matchMedia && window.matchMedia('(prefers-color-scheme: dark)').matches
+          },
+          selected: '',
+          alertOpen: false,
+          storageAccess: false,
+          preference: undefined,
+          isSystemDefaultDark: false,
+          setPreference(preference) {
+            if (!this.storageAccess) {
+              if (!window.confirm("We will remember your choice in your browser's LocalStorage. Allow this?")) {
+                return;
+              }
+              localStorage.setItem('storageAccess', true)
+              storageAccess = true;
+            }
+
+            this.selected = preference;
+            this.preference = preference
+            localStorage.setItem('theme', preference)
+
+            if (preference === 'dark') {
+              document.body.classList.add("dark");
+            }
+            if (preference === 'light') {
+              document.body.classList.remove("dark");
+            }
+            if (preference === 'system') {
+              if (this.isSystemDefaultDark) {
+                document.body.classList.add("dark");
+              } else {
+                document.body.classList.remove("dark");
+              }
+              localStorage.removeItem('theme')
+              return
+            }
+          },
+        })
+      })
+    </script>
 
-</div>
+  </footer>
+
+  <script>
+    function scrollToTop() {
+      window.scrollTo(0, 0);
+    }
+
+    window.onscroll = function() {
+      showScrollButton();
+    };
+
+    function showScrollButton() {
+      if (document.body.scrollTop > 20 || document.documentElement.scrollTop > 20) {
+        document.getElementById("scrollToTop").style.display = "block";
+      } else {
+        document.getElementById("scrollToTop").style.display = "none";
+      }
+    }
+  </script>
 
 </body>
-</html>
+
+</html>
\ No newline at end of file
diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html
index 42a56ad8e9..d6ec9f8e85 100644
--- a/doc/common/styles/html/coqremote/header.html
+++ b/doc/common/styles/html/coqremote/header.html
@@ -1,42 +1,277 @@
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
+<!DOCTYPE html>
+<html lang="en">
 
-<head>
-<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
-<link rel="shortcut icon" href="/favicon.ico" type="image/x-icon" />
-<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/node/node.css" />
-<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/defaults.css" />
-<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/system.css" />
-<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/user/user.css" />
-<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/style.css" />
-<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/coqdoc.css" />
+<head id="htmx-head">
+  <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
 
-<title>Standard Library | The Coq Proof Assistant</title>
+  <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
+  <meta name="description" content="Rocq Standard Library">
+  <meta name="twitter:title" content="Rocq Standard Library">
+  <meta name="twitter:description" content="Rocq Standard Library">
+  <meta name="twitter:image" content="https://rocq-prover.org/img/social/rocq-prover_org_social_media.png">
 
+  <meta property="og:site_name" content="Rocq">
+  <meta property="og:type" content="object">
+  <meta property="og:title" content="Rocq Standard Library">
+  <meta property="og:description" content="Rocq Standard Library">
+  <meta name="og:image" content="https://rocq-prover.org/img/social/rocq-prover_org_social_media.png">
+  <meta name="theme-color" content="#fff">
+  <meta name="color-scheme" content="white">
+
+  <meta name="ahrefs-site-verification" content="6ff715b377cdcd566334b44ae8888791189ce24640c8a403eacdc3bcbaa9449b">
+  <link rel="canonical" href="https://rocq-prover.org/doc">
+  <link rel="icon" type="image/x-icon" href="https://rocq-prover.org/logos/favicon_stdlib.ico">
+  <link rel="manifest" href="https://rocq-prover.org/manifest.json">
+
+
+  <link rel="stylesheet" href="https://rocq-prover.org/vendors/font-files/instrument-rocq.css">
+  <link rel="stylesheet" href="https://rocq-prover.org/vendors/font-files/source-code-pro.css">
+  <script defer="" src="https://rocq-prover.org/vendors/alpine-clipboard.js"></script>
+  <script defer="" src="https://rocq-prover.org/vendors/alpine.min.js"></script>
+  <script defer="" src="https://rocq-prover.org/vendors/htmx.min.js"></script>
+  <script defer="" data-domain="rocq-prover.org" src="https://rocq-prover.org/vendors/script.js"></script>
+
+  <link type="text/css" rel="stylesheet" media="all" href="https://rocq-prover.org/css/stdlib.css">
+
+
+
+  <link rel="search" href="http://rocq-prover.org/opensearch.xml" type="application/opensearchdescription+xml" title="Rocq">
+  <title>Rocq Standard Library</title>
+  <style>
+    .htmx-indicator {
+      opacity: 0;
+      transition: opacity 200ms ease-in;
+    }
+
+    .htmx-request .htmx-indicator {
+      opacity: 1
+    }
+
+    .htmx-request.htmx-indicator {
+      opacity: 1
+    }
+  </style>
 </head>
 
-<body>
-
-<div id="container">
-  <div id="headertop">
-    <div id="nav">
-      <ul class="links-menu">
-        <li><a href="//coq.inria.fr/" class="active">Home</a></li>
-        <li><a href="//coq.inria.fr/about-coq" title="More about coq">About Coq</a></li>
-        <li><a href="//coq.inria.fr/download">Get Coq</a></li>
-        <li><a href="//coq.inria.fr/documentation">Documentation</a></li>
-        <li><a href="//coq.inria.fr/community">Community</a></li>
+
+<body style="overscroll-behavior-x: auto;">
+  <script>
+    if (localStorage.theme === 'dark' || (!('theme' in localStorage) && window.matchMedia && window.matchMedia('(prefers-color-scheme: dark)').matches)) {
+      document.body.classList.add("dark");
+    } else {
+      document.body.classList.remove("dark");
+    }
+  </script>
+
+
+  <header class="fixed top-0 z-50 w-full h-20 flex items-center flex-wrap" x-data="{ open: false }">
+
+    <nav class="bg-background container-fluid dark:bg-dark-background_navigation flex gap-5 h-20 header items-center justify-between rounded-b-lg shadow-sm wide xl:gap-8">
+      <ul class="order-0 space space-x-5 xl:space-x-8 items-center flex text-content font-medium dark:text-title dark:text-opacity-60 dark:font-semibold">
+        <li style="width:170px">
+          <a href="http://rocq-prover.org/" class="block">
+            <img src="https://rocq-prover.org/logos/logo-rocq-stdlib.svg" width="170" alt="Rocq stdlib logo" class="dark:hidden">
+            <img src="https://rocq-prover.org/logos/logo-rocq-stdlib-dark.svg" width="170" alt="Rocq stdlib logo" class="hidden dark:inline">
+          </a>
+        </li>
       </ul>
+      <ul class="order-1 mr-auto items-center hidden lg:flex font-medium dark:text-white dark:text-opacity-60 dark:font-semibold">
+
+        <li><a href="http://rocq-prover.org/docs" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">Learn</a>
+
+
+        </li>
+
+        <li><a href="http://rocq-prover.org/platform" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-primary dark:text-dark-primary">Platform</a>
+
+
+        </li>
+
+        <li><a href="http://rocq-prover.org/packages" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">Packages</a>
+
+
+        </li>
+
+        <li><a href="http://rocq-prover.org/community" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">Community</a>
+
+
+        </li>
+
+        <li><a href="http://rocq-prover.org/consortium" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">Consortium</a>
+
+
+        </li>
+
+        <li><a href="http://rocq-prover.org/changelog" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">News</a>
+
+
+        </li>
+
+        <li><a href="https://x80.org/rhino-down/" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">Play</a>
+
+
+        </li>
+
+      </ul>
+
+      <ul class="order-1 lg:hidden flex items-center">
+        <li class="h-12 w-12 hover:bg-tertiary_25 dark:hover:bg-primary_20 flex items-center justify-center rounded-full text-content dark:text-dark-title">
+          <button aria-label="open menu" @click="open = ! open">
+            <svg xmlns="http://www.w3.org/2000/svg" class="h-8 w-8" fill="none" viewBox="0 0 24 24" stroke="currentColor" aria-hidden="true">
+              <path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M4 6h16M4 12h16M4 18h16"></path>
+            </svg>
+
+
+          </button>
+        </li>
+      </ul>
+    </nav>
+
+    <div class="bg-black fixed w-full h-full left-0 top-0 opacity-60 z-40" x-show="open" style="display: none;"></div>
+
+    <nav class="z-50 h-full fixed right-0 top-0 max-w-full w-96 bg-background dark:bg-dark-background shadow-lg" x-show="open" @click.away="open = false" x-transition:enter="transition duration-200 ease-out" x-transition:enter-start="translate-x-full" x-transition:leave="transition duration-100 ease-in" x-transition:leave-end="translate-x-full" style="display: none;">
+      <ul class="text-content p-6 font-semibold">
+        <li class="flex justify-between items-center">
+          <a href="http://rocq-prover.org/">
+            <img src="https://rocq-prover.org/logos/logo-rocq-blue_orange.svg" width="132" alt="Rocq logo" class="dark:hidden">
+            <img src="https://rocq-prover.org/logos/logo-rocq-white.svg" width="132" alt="Rocq logo" class="hidden dark:inline">
+          </a>
+          <div class="" x-on:click="open = false">
+            <button aria-label="close" class="text-content dark:text-dark-title">
+              <svg xmlns="http://www.w3.org/2000/svg" class="h-8 w-8" fill="none" viewBox="0 0 24 24" stroke="currentColor" aria-hidden="true">
+                <path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M6 18L18 6M6 6l12 12"></path>
+              </svg>
+
+
+            </button>
+          </div>
+        </li>
+
+        <li><a href="http://rocq-prover.org/docs" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">Learn</a>
+
+
+        </li>
+
+        <li><a href="http://rocq-prover.org/platform" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-primary dark:text-dark-primary">Platform</a>
+
+
+        </li>
+
+        <li><a href="http://rocq-prover.org/packages" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">Packages</a>
+
+
+        </li>
+
+        <li><a href="http://rocq-prover.org/community" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">Community</a>
+
+
+        </li>
+
+        <li><a href="http://rocq-prover.org/consortium" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">Consortium</a>
+
+
+        </li>
+
+        <li><a href="http://rocq-prover.org/changelog" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">News</a>
+
+
+        </li>
+
+        <li><a href="https://x80.org/rhino-down/" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primaryblock text-title dark:text-dark-title">Play</a>
+
+
+        </li>
+
+        <li class="mt-3 mb-6">
+          <a href="http://rocq-prover.org/docs#beginner_section" class="w-full rounded font-normal py-3 px-7 flex items-center justify-center bg-primary dark:bg-dark-primary text-white dark:text-dark-title">Get started</a>
+        </li>
+        <li>
+          <div class="space-x-6 text-2xl flex items-center">
+            <a aria-label="Rocq&#39;s Zulip" href="https://coq.zulipchat.com/" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
+              <svg viewBox="0 0 256 256" version="1.1" class="w-6 h-6" fill="currentColor" aria-hidden="true" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" preserveAspectRatio="xMidYMid">
+                <path d="M128,0 C198.692448,0 256,57.307552 256,128 C256,198.692448 198.692448,256 128,256 C57.307552,256 0,198.692448 0,128 C0,57.307552 57.307552,0 128,0 Z M121.679533,118.222163 L75.7877336,159.200897 C71.0603547,162.920702 67.9584879,169.060511 67.9584879,175.967416 C67.9584879,187.245548 76.232162,196.475047 86.3444303,196.475047 L172.590938,196.475047 C182.703207,196.475047 190.976881,187.245548 190.976881,175.967416 C190.976881,164.68624 182.703207,155.459784 172.590938,155.459784 L107.299534,155.459784 C106.331533,155.459784 105.719683,154.300009 106.191507,153.356359 L123.024994,119.652857 C123.639888,118.669635 122.531861,117.491595 121.679533,118.222163 Z M172.590938,59.3627915 L86.3444303,59.3627915 C76.232162,59.3627915 67.9584879,68.58925 67.9584879,79.870426 C67.9584879,91.1485579 76.232162,100.378058 86.3444303,100.378058 L86.3444303,100.378058 L151.635834,100.378058 C152.603836,100.378058 153.215686,101.537833 152.743861,102.481482 L152.743861,102.481482 L135.910374,136.184985 C135.29548,137.168207 136.403507,138.346246 137.255836,137.615679 L137.255836,137.615679 L183.147635,96.6308563 C187.875014,92.9080074 190.976881,86.7712425 190.976881,79.8643379 C190.976881,68.586206 182.703207,59.3567064 172.590938,59.3627915 L172.590938,59.3627915 Z" fill="inherit"></path>
+              </svg>
+
+
+            </a>
+            <a aria-label="Rocq&#39;s Discourse" href="https://coq.discourse.group/" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
+              <svg xmlns="http://www.w3.org/2000/svg" class="w-6 h-6" fill="currentColor" viewBox="0 0 448 512" aria-hidden="true">
+                <path d="M225.9 32C103.3 32 0 130.5 0 252.1 0 256 .1 480 .1 480l225.8-.2c122.7 0 222.1-102.3 222.1-223.9C448 134.3 348.6 32 225.9 32zM224 384c-19.4 0-37.9-4.3-54.4-12.1L88.5 392l22.9-75c-9.8-18.1-15.4-38.9-15.4-61 0-70.7 57.3-128 128-128s128 57.3 128 128-57.3 128-128 128z"></path>
+              </svg>
+
+
+
+            </a>
+            <a aria-label="The Rocq Prover on GitHub" href="https://github.com/coq/coq" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
+              <svg xmlns="http://www.w3.org/2000/svg" class="w-6 h-6" fill="currentColor" viewBox="0 0 24 24" aria-hidden="true">
+                <path fill-rule="evenodd" d="M12 2C6.477 2 2 6.484 2 12.017c0 4.425 2.865 8.18 6.839 9.504.5.092.682-.217.682-.483 0-.237-.008-.868-.013-1.703-2.782.605-3.369-1.343-3.369-1.343-.454-1.158-1.11-1.466-1.11-1.466-.908-.62.069-.608.069-.608 1.003.07 1.531 1.032 1.531 1.032.892 1.53 2.341 1.088 2.91.832.092-.647.35-1.088.636-1.338-2.22-.253-4.555-1.113-4.555-4.951 0-1.093.39-1.988 1.029-2.688-.103-.253-.446-1.272.098-2.65 0 0 .84-.27 2.75 1.026A9.564 9.564 0 0112 6.844c.85.004 1.705.115 2.504.337 1.909-1.296 2.747-1.027 2.747-1.027.546 1.379.202 2.398.1 2.651.64.7 1.028 1.595 1.028 2.688 0 3.848-2.339 4.695-4.566 4.943.359.309.678.92.678 1.855 0 1.338-.012 2.419-.012 2.747 0 .268.18.58.688.482A10.019 10.019 0 0022 12.017C22 6.484 17.522 2 12 2z" clip-rule="evenodd"></path>
+              </svg>
+
+
+            </a>
+            <a aria-label="The Rocq Prover on Mastodon" rel="me" href="https://mastodon.acm.org/@RocqProver" class="opacity-60 hover:opacity-100 text-content dark:text-dark-title hover:text-primary dark:hover:text-dark-primary">
+              <svg viewBox="0 0 74 79" class="w-6 h-6" fill="currentColor" xmlns="http://www.w3.org/2000/svg" aria-hidden="true">
+                <path d="M73.7014 17.4323C72.5616 9.05152 65.1774 2.4469 56.424 1.1671C54.9472 0.950843 49.3518 0.163818 36.3901 0.163818H36.2933C23.3281 0.163818 20.5465 0.950843 19.0697 1.1671C10.56 2.41145 2.78877 8.34604 0.903306 16.826C-0.00357854 21.0022 -0.100361 25.6322 0.068112 29.8793C0.308275 35.9699 0.354874 42.0498 0.91406 48.1156C1.30064 52.1448 1.97502 56.1419 2.93215 60.0769C4.72441 67.3445 11.9795 73.3925 19.0876 75.86C26.6979 78.4332 34.8821 78.8603 42.724 77.0937C43.5866 76.8952 44.4398 76.6647 45.2833 76.4024C47.1867 75.8033 49.4199 75.1332 51.0616 73.9562C51.0841 73.9397 51.1026 73.9184 51.1156 73.8938C51.1286 73.8693 51.1359 73.8421 51.1368 73.8144V67.9366C51.1364 67.9107 51.1302 67.8852 51.1186 67.862C51.1069 67.8388 51.0902 67.8184 51.0695 67.8025C51.0489 67.7865 51.0249 67.7753 50.9994 67.7696C50.9738 67.764 50.9473 67.7641 50.9218 67.7699C45.8976 68.9569 40.7491 69.5519 35.5836 69.5425C26.694 69.5425 24.3031 65.3699 23.6184 63.6327C23.0681 62.1314 22.7186 60.5654 22.5789 58.9744C22.5775 58.9477 22.5825 58.921 22.5934 58.8965C22.6043 58.8721 22.621 58.8505 22.6419 58.8336C22.6629 58.8167 22.6876 58.8049 22.714 58.7992C22.7404 58.7934 22.7678 58.794 22.794 58.8007C27.7345 59.9796 32.799 60.5746 37.8813 60.5733C39.1036 60.5733 40.3223 60.5733 41.5447 60.5414C46.6562 60.3996 52.0437 60.1408 57.0728 59.1694C57.1983 59.1446 57.3237 59.1233 57.4313 59.0914C65.3638 57.5847 72.9128 52.8555 73.6799 40.8799C73.7086 40.4084 73.7803 35.9415 73.7803 35.4523C73.7839 33.7896 74.3216 23.6576 73.7014 17.4323ZM61.4925 47.3144H53.1514V27.107C53.1514 22.8528 51.3591 20.6832 47.7136 20.6832C43.7061 20.6832 41.6988 23.2499 41.6988 28.3194V39.3803H33.4078V28.3194C33.4078 23.2499 31.3969 20.6832 27.3894 20.6832C23.7654 20.6832 21.9552 22.8528 21.9516 27.107V47.3144H13.6176V26.4937C13.6176 22.2395 14.7157 18.8598 16.9118 16.3545C19.1772 13.8552 22.1488 12.5719 25.8373 12.5719C30.1064 12.5719 33.3325 14.1955 35.4832 17.4394L37.5587 20.8853L39.6377 17.4394C41.7884 14.1955 45.0145 12.5719 49.2765 12.5719C52.9614 12.5719 55.9329 13.8552 58.2055 16.3545C60.4017 18.8574 61.4997 22.2371 61.4997 26.4937L61.4925 47.3144Z" fill="inherit"></path>
+              </svg>
+
+
+            </a>
+          </div>
+        </li>
+      </ul>
+    </nav>
+  </header>
+  <script>
+    window.addEventListener('keydown', function(event) {
+      if (event.key === "/") {
+        event.preventDefault();
+        document.querySelector("input[type='search']").focus()
+      }
+    })
+  </script>
+
+  <main class="bg-background dark:bg-dark-background pt-[80px]">
+    <nav aria-label="breadcrumbs" class="px-4 flex bg-title dark:bg-[#111827] text-white dark:text-dark-title md:hidden">
+      <ul>
+        <li class="inline-block">
+          <a href="http://rocq-prover.org/stdlib" class="flex items-center px-2 py-2 border-transparent border-2 border-b-4"> Standard Library
+            <span> <svg xmlns="http://www.w3.org/2000/svg" class="w-3 h-3 ml-2" fill="none" viewBox="0 0 24 24" stroke-width="1.5" stroke="currentColor" aria-hidden="true">
+                <path stroke-linecap="round" stroke-linejoin="round" d="M8.25 4.5l7.5 7.5-7.5 7.5"></path>
+              </svg>
+
+            </span> </a>
+        </li>
+        <li class="inline-block">
+          <select onchange="location = this.value;" class="appearance-none border-2 border-b-4 bg-transparent bg-none font-bold border-none w-auto p-0 m-0 cursor-pointer focus:outline-none focus:ring-0">
+            <option value="index.html" selected="">
+              Table of contents
+            </option>
+            <option value="genindex.html">
+              Index
+            </option>
+
+          </select>
+          <span class="text-primary dark:text-dark-primary cursor-pointer">▾</span>
+        </li>
+      </ul>
+    </nav>
+    <div class="hidden md:flex">
+      <nav class="lg:-mt-[10px] lg:pt-[10px] bg-secondary dark:bg-[#111827] rounded-b-lg container-fluid wide flex flex-wrap">
+        <a href="index.html" class="justify-start px-4 py-2 text-white dark:text-dark-title items-center font-normal border-2 border-b-4 border-transparent rounded border-b-primary dark:border-b-dark-primary">
+          Table of contents
+        </a>
+        <a href="genindex.html" class="justify-start px-4 py-2 text-white dark:text-dark-title items-center font-normal border-2 border-b-4 border-transparent rounded opacity-80 hover:text-primary dark:hover:text-dark-primary">
+          Index
+        </a>
+      </nav>
     </div>
-  </div>
-
-  <div id="header">
-    <div id="logoWrapper">
-      <div id="logo"><a href="//coq.inria.fr/" title="Home"><img src="//coq.inria.fr/files/barron_logo.png" alt="Home" /></a>
-      </div>
-      <div id="siteName"><a href="//coq.inria.fr/" title="Home">The Coq Proof Assistant</a>
-      </div>
-    </div>
-  </div>
 
-  <div id="content">
+
+    <div class="bg-background dark:bg-dark-background">
+      <div class="flex-1 z-0 z- min-w-0 pb-12">
+        <div class="bg-background dark:bg-dark-background">
+          <div class="container-fluid dark:text-dark-content prose pt-10 stdlib text-content">
+          
+          <!-- ************************
+            END STDLIB HEADER
+          ************************* -->
\ No newline at end of file

From c201bab60cc2f36cb7c42c7f5ec5ce86045f46ed Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 24 Jan 2025 21:31:42 +0100
Subject: [PATCH 2/3] Update header.html

Remove playground option, disabled for now
---
 doc/common/styles/html/coqremote/header.html | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html
index d6ec9f8e85..c12dc2a2c1 100644
--- a/doc/common/styles/html/coqremote/header.html
+++ b/doc/common/styles/html/coqremote/header.html
@@ -104,14 +104,6 @@
 
         <li><a href="http://rocq-prover.org/changelog" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">News</a>
 
-
-        </li>
-
-        <li><a href="https://x80.org/rhino-down/" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">Play</a>
-
-
-        </li>
-
       </ul>
 
       <ul class="order-1 lg:hidden flex items-center">
@@ -274,4 +266,4 @@
           
           <!-- ************************
             END STDLIB HEADER
-          ************************* -->
\ No newline at end of file
+          ************************* -->

From c3c413ddde7036682995635f4a70df4ff6fb6c49 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 24 Jan 2025 21:33:12 +0100
Subject: [PATCH 3/3] Update header.html

Restore missing closing tag
---
 doc/common/styles/html/coqremote/header.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html
index c12dc2a2c1..c40834158a 100644
--- a/doc/common/styles/html/coqremote/header.html
+++ b/doc/common/styles/html/coqremote/header.html
@@ -103,7 +103,7 @@
         </li>
 
         <li><a href="http://rocq-prover.org/changelog" class="block font-normal py-3 mg:py-4 px-1 lg:px-3 hover:text-primary dark:hover:text-dark-primary text-title dark:text-dark-title">News</a>
-
+        </li>
       </ul>
 
       <ul class="order-1 lg:hidden flex items-center">