Update from https://github.com/SkyLabsAI/ci/actions/runs/27824637239/attempts/1

Author: rlepigre-skylabs-ai

docs/_static/coqdoc/test.html/index.html

@@ -47,7 +47,7 @@
 <td>Z</td>
 <td><a href="index.html#global__">_</a></td>
 <td>other</td>
-<td>(49 entries)</td>
+<td>(51 entries)</td>
 </tr>
 <tr>
 <td>Module Index</td>
@@ -79,7 +79,7 @@
 <td>Z</td>
 <td><a href="index.html#module__">_</a></td>
 <td>other</td>
-<td>(12 entries)</td>
+<td>(13 entries)</td>
 </tr>
 <tr>
 <td>Library Index</td>
@@ -303,7 +303,7 @@
 <td>Z</td>
 <td><a href="index.html#definition__">_</a></td>
 <td>other</td>
-<td>(14 entries)</td>
+<td>(15 entries)</td>
 </tr>
 <tr>
 <td>Record Index</td>
@@ -377,6 +377,8 @@ <h1>Global Index</h1>
 <br/><br/><a id="global_P"></a><h2>P </h2>
 <a href="test.prelude.html">prelude</a> [library]<br/>
 <br/><br/><a id="global_S"></a><h2>S </h2>
+<a href="test.constr.html#SpecializeProducts_Tests.Unnamed_thm">SpecializeProducts_Tests.Unnamed_thm</a> [definition, in <a href="test.constr.html">test.constr</a>]<br/>
+<a href="test.constr.html#SpecializeProducts_Tests">SpecializeProducts_Tests</a> [module, in <a href="test.constr.html">test.constr</a>]<br/>
 <a href="test.control.html#State_test.Unnamed_thm">State_test.Unnamed_thm</a> [definition, in <a href="test.control.html">test.control</a>]<br/>
 <a href="test.control.html#State_test">State_test</a> [module, in <a href="test.control.html">test.control</a>]<br/>
 <a href="test.level_env.html#Substitute">Substitute</a> [module, in <a href="test.level_env.html">test.level_env</a>]<br/>
@@ -414,6 +416,7 @@ <h1>Module Index</h1>
 <br/><br/><a id="module_E"></a><h2>E </h2>
 <a href="test.constr.html#Evar_Test">Evar_Test</a> [in <a href="test.constr.html">test.constr</a>]<br/>
 <br/><br/><a id="module_S"></a><h2>S </h2>
+<a href="test.constr.html#SpecializeProducts_Tests">SpecializeProducts_Tests</a> [in <a href="test.constr.html">test.constr</a>]<br/>
 <a href="test.control.html#State_test">State_test</a> [in <a href="test.control.html">test.control</a>]<br/>
 <a href="test.level_env.html#Substitute">Substitute</a> [in <a href="test.level_env.html">test.level_env</a>]<br/>
 <br/><br/><a id="module_T"></a><h2>T </h2>
@@ -479,6 +482,7 @@ <h1>Definition Index</h1>
 <br/><br/><a id="definition_E"></a><h2>E </h2>
 <a href="test.constr.html#Evar_Test.Unnamed_thm">Evar_Test.Unnamed_thm</a> [in <a href="test.constr.html">test.constr</a>]<br/>
 <br/><br/><a id="definition_S"></a><h2>S </h2>
+<a href="test.constr.html#SpecializeProducts_Tests.Unnamed_thm">SpecializeProducts_Tests.Unnamed_thm</a> [in <a href="test.constr.html">test.constr</a>]<br/>
 <a href="test.control.html#State_test.Unnamed_thm">State_test.Unnamed_thm</a> [in <a href="test.control.html">test.control</a>]<br/>
 <a href="test.level_env.html#Substitute.Unnamed_thm1">Substitute.Unnamed_thm1</a> [in <a href="test.level_env.html">test.level_env</a>]<br/>
 <a href="test.level_env.html#Substitute.Unnamed_thm0">Substitute.Unnamed_thm0</a> [in <a href="test.level_env.html">test.level_env</a>]<br/>
@@ -528,7 +532,7 @@ <h1>Record Index</h1>
 <td>Z</td>
 <td><a href="index.html#global__">_</a></td>
 <td>other</td>
-<td>(49 entries)</td>
+<td>(51 entries)</td>
 </tr>
 <tr>
 <td>Module Index</td>
@@ -560,7 +564,7 @@ <h1>Record Index</h1>
 <td>Z</td>
 <td><a href="index.html#module__">_</a></td>
 <td>other</td>
-<td>(12 entries)</td>
+<td>(13 entries)</td>
 </tr>
 <tr>
 <td>Library Index</td>
@@ -784,7 +788,7 @@ <h1>Record Index</h1>
 <td>Z</td>
 <td><a href="index.html#definition__">_</a></td>
 <td>other</td>
-<td>(14 entries)</td>
+<td>(15 entries)</td>
 </tr>
 <tr>
 <td>Record Index</td>

docs/_static/coqdoc/test.html/test.constr.html

@@ -176,6 +176,18 @@ <h1 class="libtitle">Library test.constr</h1>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="test.constr.html#Evar_Test"><span class="id" title="module">Evar_Test</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a id="SpecializeProducts_Tests" class="idref" href="#SpecializeProducts_Tests"><span class="id" title="module">SpecializeProducts_Tests</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Import</span> <span class="id" title="module">Ltac2</span> <span class="id" title="module">Constr</span>.<br/>
+
+<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Goal</span> <a id="SpecializeProducts_Tests.Unnamed_thm" class="idref" href="#SpecializeProducts_Tests.Unnamed_thm"><span class="id" title="definition">True</span></a>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">_</span> := <span class="id" title="var">specialize_products</span> '(<span class="id" title="keyword">forall</span> <a id="A:19" class="idref" href="#A:19"><span class="id" title="binder">A</span></a> : <span class="id" title="keyword">Type</span>, <a class="idref" href="test.constr.html#A:19"><span class="id" title="variable">A</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.2/corelib//Corelib.Init.Notations.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="test.constr.html#A:19"><span class="id" title="variable">A</span></a>)<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[| <span class="id" title="var">open_constr</span>:(<span class="id" title="var">_</span>); <span class="id" title="var">open_constr</span>:(<span class="id" title="var">_</span>) |] <span class="id" title="tactic">in</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">exact</span> <a class="idref" href="http://rocq-prover.org/doc/V9.2/corelib//Corelib.Init.Logic.html#I"><span class="id" title="constructor">I</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Abort</span>.<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="test.constr.html#SpecializeProducts_Tests"><span class="id" title="module">SpecializeProducts_Tests</span></a>.<br/>
 </div>
 </div>