Documentation of branch “v9.0” at 8918ea10

coq · Jan 15, 2025 · dc9b7df · dc9b7df
1 parent 9584d22
commit dc9b7df
Show file tree

Hide file tree

Showing 249 changed files with 1,192 additions and 1,192 deletions.
diff --git a/v9.0/refman/.doctrees/addendum/extraction.doctree b/v9.0/refman/.doctrees/addendum/extraction.doctree
diff --git a/v9.0/refman/.doctrees/addendum/generalized-rewriting.doctree b/v9.0/refman/.doctrees/addendum/generalized-rewriting.doctree
diff --git a/v9.0/refman/.doctrees/addendum/implicit-coercions.doctree b/v9.0/refman/.doctrees/addendum/implicit-coercions.doctree
diff --git a/v9.0/refman/.doctrees/addendum/micromega.doctree b/v9.0/refman/.doctrees/addendum/micromega.doctree
diff --git a/v9.0/refman/.doctrees/addendum/miscellaneous-extensions.doctree b/v9.0/refman/.doctrees/addendum/miscellaneous-extensions.doctree
diff --git a/v9.0/refman/.doctrees/addendum/program.doctree b/v9.0/refman/.doctrees/addendum/program.doctree
diff --git a/v9.0/refman/.doctrees/addendum/rewrite-rules.doctree b/v9.0/refman/.doctrees/addendum/rewrite-rules.doctree
diff --git a/v9.0/refman/.doctrees/addendum/ring.doctree b/v9.0/refman/.doctrees/addendum/ring.doctree
diff --git a/v9.0/refman/.doctrees/addendum/sprop.doctree b/v9.0/refman/.doctrees/addendum/sprop.doctree
diff --git a/v9.0/refman/.doctrees/addendum/type-classes.doctree b/v9.0/refman/.doctrees/addendum/type-classes.doctree
diff --git a/v9.0/refman/.doctrees/addendum/universe-polymorphism.doctree b/v9.0/refman/.doctrees/addendum/universe-polymorphism.doctree
diff --git a/v9.0/refman/.doctrees/changes.doctree b/v9.0/refman/.doctrees/changes.doctree
diff --git a/v9.0/refman/.doctrees/environment.pickle b/v9.0/refman/.doctrees/environment.pickle
diff --git a/v9.0/refman/.doctrees/language/cic.doctree b/v9.0/refman/.doctrees/language/cic.doctree
diff --git a/v9.0/refman/.doctrees/language/coq-library.doctree b/v9.0/refman/.doctrees/language/coq-library.doctree
diff --git a/v9.0/refman/.doctrees/language/core/assumptions.doctree b/v9.0/refman/.doctrees/language/core/assumptions.doctree
diff --git a/v9.0/refman/.doctrees/language/core/basic.doctree b/v9.0/refman/.doctrees/language/core/basic.doctree
diff --git a/v9.0/refman/.doctrees/language/core/coinductive.doctree b/v9.0/refman/.doctrees/language/core/coinductive.doctree
diff --git a/v9.0/refman/.doctrees/language/core/conversion.doctree b/v9.0/refman/.doctrees/language/core/conversion.doctree
diff --git a/v9.0/refman/.doctrees/language/core/inductive.doctree b/v9.0/refman/.doctrees/language/core/inductive.doctree
diff --git a/v9.0/refman/.doctrees/language/core/modules.doctree b/v9.0/refman/.doctrees/language/core/modules.doctree
diff --git a/v9.0/refman/.doctrees/language/core/primitive.doctree b/v9.0/refman/.doctrees/language/core/primitive.doctree
diff --git a/v9.0/refman/.doctrees/language/core/records.doctree b/v9.0/refman/.doctrees/language/core/records.doctree
diff --git a/v9.0/refman/.doctrees/language/core/sections.doctree b/v9.0/refman/.doctrees/language/core/sections.doctree
diff --git a/v9.0/refman/.doctrees/language/core/variants.doctree b/v9.0/refman/.doctrees/language/core/variants.doctree
diff --git a/v9.0/refman/.doctrees/language/extensions/arguments-command.doctree b/v9.0/refman/.doctrees/language/extensions/arguments-command.doctree
diff --git a/v9.0/refman/.doctrees/language/extensions/canonical.doctree b/v9.0/refman/.doctrees/language/extensions/canonical.doctree
diff --git a/v9.0/refman/.doctrees/language/extensions/evars.doctree b/v9.0/refman/.doctrees/language/extensions/evars.doctree
diff --git a/v9.0/refman/.doctrees/language/extensions/implicit-arguments.doctree b/v9.0/refman/.doctrees/language/extensions/implicit-arguments.doctree
diff --git a/v9.0/refman/.doctrees/language/extensions/match.doctree b/v9.0/refman/.doctrees/language/extensions/match.doctree
diff --git a/v9.0/refman/.doctrees/practical-tools/coq-commands.doctree b/v9.0/refman/.doctrees/practical-tools/coq-commands.doctree
diff --git a/v9.0/refman/.doctrees/practical-tools/coqide.doctree b/v9.0/refman/.doctrees/practical-tools/coqide.doctree
diff --git a/v9.0/refman/.doctrees/proof-engine/ltac.doctree b/v9.0/refman/.doctrees/proof-engine/ltac.doctree
diff --git a/v9.0/refman/.doctrees/proof-engine/ltac2.doctree b/v9.0/refman/.doctrees/proof-engine/ltac2.doctree
diff --git a/v9.0/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree b/v9.0/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree
diff --git a/v9.0/refman/.doctrees/proof-engine/tactics.doctree b/v9.0/refman/.doctrees/proof-engine/tactics.doctree
diff --git a/v9.0/refman/.doctrees/proof-engine/vernacular-commands.doctree b/v9.0/refman/.doctrees/proof-engine/vernacular-commands.doctree
diff --git a/v9.0/refman/.doctrees/proofs/automatic-tactics/auto.doctree b/v9.0/refman/.doctrees/proofs/automatic-tactics/auto.doctree
diff --git a/v9.0/refman/.doctrees/proofs/automatic-tactics/logic.doctree b/v9.0/refman/.doctrees/proofs/automatic-tactics/logic.doctree
diff --git a/v9.0/refman/.doctrees/proofs/writing-proofs/equality.doctree b/v9.0/refman/.doctrees/proofs/writing-proofs/equality.doctree
diff --git a/v9.0/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree b/v9.0/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree
diff --git a/v9.0/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree b/v9.0/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree
diff --git a/v9.0/refman/.doctrees/user-extensions/syntax-extensions.doctree b/v9.0/refman/.doctrees/user-extensions/syntax-extensions.doctree
diff --git a/v9.0/refman/.doctrees/using/libraries/funind.doctree b/v9.0/refman/.doctrees/using/libraries/funind.doctree
diff --git a/v9.0/refman/.doctrees/using/libraries/writing.doctree b/v9.0/refman/.doctrees/using/libraries/writing.doctree
diff --git a/v9.0/refman/proof-engine/ltac.html b/v9.0/refman/proof-engine/ltac.html
@@ -4286,42 +4286,42 @@ <h3>Profiling <code class="docutils literal notranslate"><span class="pre">L</sp
 </span></dt><dd><span>No more goals.
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Show</span><span> </span><span class="coqdoc-keyword">Ltac</span><span> </span><span class="coqdoc-var">Profile</span><span>.</span><span>
-</span></dt><dd><span>total time:      1.066s
+</span></dt><dd><span>total time:      0.892s
 
  tactic                                      local  total   calls       max
 ───────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac --------------------------------------   0.1% 100.0%       1    1.066s
-─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  93.1%      26    0.070s
-─&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  93.0%      26    0.070s
-─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  93.0%      26    0.070s
-─t_tauto_intuit ---------------------------   0.1%  92.9%      26    0.070s
-─&lt;Corelib.Init.Tauto.simplif&gt; -------------  60.2%  89.3%      26    0.069s
-─&lt;Corelib.Init.Tauto.is_conj&gt; -------------  22.2%  22.2%   28756    0.010s
-─lia --------------------------------------   0.1%   6.6%      28    0.049s
-─Zify.zify --------------------------------   4.9%   5.4%      54    0.049s
-─&lt;Corelib.Init.Tauto.axioms&gt; --------------   2.5%   3.5%       0    0.005s
-─elim id ----------------------------------   3.5%   3.5%     650    0.000s
+─tac --------------------------------------   0.1% 100.0%       1    0.892s
+─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.4%      26    0.064s
+─&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  92.3%      26    0.064s
+─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  92.3%      26    0.064s
+─t_tauto_intuit ---------------------------   0.1%  92.1%      26    0.064s
+─&lt;Corelib.Init.Tauto.simplif&gt; -------------  57.8%  88.6%      26    0.063s
+─&lt;Corelib.Init.Tauto.is_conj&gt; -------------  24.6%  24.6%   28756    0.009s
+─lia --------------------------------------   0.1%   7.4%      28    0.047s
+─Zify.zify --------------------------------   5.5%   6.1%      54    0.047s
+─&lt;Corelib.Init.Tauto.axioms&gt; --------------   2.4%   3.5%       0    0.003s
+─elim id ----------------------------------   2.9%   2.9%     650    0.000s
 
  tactic                                        local  total   calls       max
 ─────────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac ----------------------------------------   0.1% 100.0%       1    1.066s
- ├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  93.1%      26    0.070s
- │└&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  93.0%      26    0.070s
- │└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  93.0%      26    0.070s
- │└t_tauto_intuit ---------------------------   0.1%  92.9%      26    0.070s
- │ ├─&lt;Corelib.Init.Tauto.simplif&gt; -----------  60.2%  89.3%      26    0.069s
- │ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; ---------  22.2%  22.2%   28756    0.010s
- │ │ └─elim id ------------------------------   3.5%   3.5%     650    0.000s
- │ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------   2.5%   3.5%       0    0.005s
- └─lia --------------------------------------   0.1%   6.6%      28    0.049s
-  └Zify.zify --------------------------------   4.9%   5.4%      54    0.049s
+─tac ----------------------------------------   0.1% 100.0%       1    0.892s
+ ├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.4%      26    0.064s
+ │└&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  92.3%      26    0.064s
+ │└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  92.3%      26    0.064s
+ │└t_tauto_intuit ---------------------------   0.1%  92.1%      26    0.064s
+ │ ├─&lt;Corelib.Init.Tauto.simplif&gt; -----------  57.8%  88.6%      26    0.063s
+ │ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; ---------  24.6%  24.6%   28756    0.009s
+ │ │ └─elim id ------------------------------   2.9%   2.9%     650    0.000s
+ │ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------   2.4%   3.5%       0    0.003s
+ └─lia --------------------------------------   0.1%   7.4%      28    0.047s
+  └Zify.zify --------------------------------   5.5%   6.1%      54    0.047s
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Show</span><span> </span><span class="coqdoc-keyword">Ltac</span><span> </span><span class="coqdoc-var">Profile</span><span> &quot;lia&quot;.</span><span>
-</span></dt><dd><span>total time:      1.066s
+</span></dt><dd><span>total time:      0.892s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘
-─lia --   0.1%   6.6%      28    0.049s
+─lia --   0.1%   7.4%      28    0.047s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘

diff --git a/v9.0/refman/proofs/writing-proofs/equality.html b/v9.0/refman/proofs/writing-proofs/equality.html
@@ -2640,15 +2640,15 @@ <h3>Computing in a term: eval and Eval<a class="headerlink" href="#computing-in-
   True
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Time</span><span> </span><span class="coqdoc-tactic">assert</span><span> (</span><span class="coqdoc-var">id</span><span> (</span><span class="coqdoc-var">fact</span><span> 8) = </span><span class="coqdoc-var">fact</span><span> 8) </span><span class="coqdoc-tactic">by</span><span> </span><span class="coqdoc-tactic">reflexivity</span><span>.</span><span>
-</span></dt><dd><span>Finished transaction in 0.081 secs (0.05u,0.03s) (successful)
+</span></dt><dd><span>Finished transaction in 0.055 secs (0.045u,0.009s) (successful)
 1 goal
 
   H : id (fact 8)</span><span> =</span><span> fact 8
   ============================
   True
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Time</span><span> </span><span class="coqdoc-tactic">assert</span><span> (</span><span class="coqdoc-var">id</span><span> (</span><span class="coqdoc-var">fact</span><span> 9) = </span><span class="coqdoc-var">fact</span><span> 9) </span><span class="coqdoc-tactic">by</span><span> </span><span class="coqdoc-tactic">reflexivity</span><span>.</span><span>
-</span></dt><dd><span>Finished transaction in 0.401 secs (0.4u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0.263 secs (0.263u,0.s) (successful)
 1 goal
 
   H : id (fact 8)</span><span> =</span><span> fact 8

diff --git a/v9.0/refman/searchindex.js b/v9.0/refman/searchindex.js
diff --git a/v9.0/stdlib/Stdlib.Arith.Arith_base.html b/v9.0/stdlib/Stdlib.Arith.Arith_base.html
@@ -57,7 +57,7 @@ <h1 class="libtitle">Library Stdlib.Arith.Arith_base</h1>
 </div>
 
 <div class="doc">
-<a id="lab1"></a><h1 class="section"><span class="inlinecode"><span class="id" title="var">arith</span></span> hint database</h1>
+<a id="lab17"></a><h1 class="section"><span class="inlinecode"><span class="id" title="var">arith</span></span> hint database</h1>
 
 </div>
 <div class="code">
@@ -79,7 +79,7 @@ <h1 class="libtitle">Library Stdlib.Arith.Arith_base</h1>
 </div>
 
 <div class="doc">
-<a id="lab2"></a><h2 class="section"><span class="inlinecode"><span class="id" title="var">lt</span></span> and <span class="inlinecode"><span class="id" title="var">le</span></span></h2>
+<a id="lab18"></a><h2 class="section"><span class="inlinecode"><span class="id" title="var">lt</span></span> and <span class="inlinecode"><span class="id" title="var">le</span></span></h2>
 
 </div>
 <div class="code">

diff --git a/v9.0/stdlib/Stdlib.Arith.EqNat.html b/v9.0/stdlib/Stdlib.Arith.EqNat.html
@@ -55,7 +55,7 @@ <h1 class="libtitle">Library Stdlib.Arith.EqNat</h1>
 Equality on natural numbers 
 <div class="paragraph"> </div>
 
-<a id="lab18"></a><h1 class="section">Propositional equality</h1>
+<a id="lab1"></a><h1 class="section">Propositional equality</h1>
 
 </div>
 <div class="code">

diff --git a/v9.0/stdlib/Stdlib.Arith.PeanoNat.html b/v9.0/stdlib/Stdlib.Arith.PeanoNat.html
@@ -148,7 +148,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab3"></a><h2 class="section">Remaining constants not defined in Stdlib.Init.Nat</h2>
+<a id="lab2"></a><h2 class="section">Remaining constants not defined in Stdlib.Init.Nat</h2>
 
 <div class="paragraph"> </div>
 
@@ -166,7 +166,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab4"></a><h2 class="section">Basic specifications : pred add sub mul</h2>
+<a id="lab3"></a><h2 class="section">Basic specifications : pred add sub mul</h2>
 
 </div>
 <div class="code">
@@ -208,7 +208,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab5"></a><h2 class="section">Boolean comparisons</h2>
+<a id="lab4"></a><h2 class="section">Boolean comparisons</h2>
 
 </div>
 <div class="code">
@@ -240,7 +240,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab6"></a><h2 class="section">Decidability of equality over <span class="inlinecode"><span class="id" title="var">nat</span></span>.</h2>
+<a id="lab5"></a><h2 class="section">Decidability of equality over <span class="inlinecode"><span class="id" title="var">nat</span></span>.</h2>
 
 </div>
 <div class="code">
@@ -252,7 +252,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab7"></a><h2 class="section">Ternary comparison</h2>
+<a id="lab6"></a><h2 class="section">Ternary comparison</h2>
 
 <div class="paragraph"> </div>
 
@@ -281,7 +281,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab8"></a><h2 class="section">Minimum, maximum</h2>
+<a id="lab7"></a><h2 class="section">Minimum, maximum</h2>
 
 </div>
 <div class="code">
@@ -331,7 +331,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab9"></a><h2 class="section">Power</h2>
+<a id="lab8"></a><h2 class="section">Power</h2>
 
 </div>
 <div class="code">
@@ -349,7 +349,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab10"></a><h2 class="section">Square</h2>
+<a id="lab9"></a><h2 class="section">Square</h2>
 
 </div>
 <div class="code">
@@ -361,7 +361,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab11"></a><h2 class="section">Parity</h2>
+<a id="lab10"></a><h2 class="section">Parity</h2>
 
 </div>
 <div class="code">
@@ -405,7 +405,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab12"></a><h2 class="section">Division</h2>
+<a id="lab11"></a><h2 class="section">Division</h2>
 
 </div>
 <div class="code">
@@ -434,7 +434,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab13"></a><h2 class="section">Square root</h2>
+<a id="lab12"></a><h2 class="section">Square root</h2>
 
 </div>
 <div class="code">
@@ -458,7 +458,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab14"></a><h2 class="section">Logarithm</h2>
+<a id="lab13"></a><h2 class="section">Logarithm</h2>
 
 </div>
 <div class="code">
@@ -480,7 +480,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab15"></a><h2 class="section">Properties of <span class="inlinecode"><span class="id" title="var">iter</span></span></h2>
+<a id="lab14"></a><h2 class="section">Properties of <span class="inlinecode"><span class="id" title="var">iter</span></span></h2>
 
 </div>
 <div class="code">
@@ -532,7 +532,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab16"></a><h2 class="section">Gcd</h2>
+<a id="lab15"></a><h2 class="section">Gcd</h2>
 
 </div>
 <div class="code">
@@ -560,7 +560,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab17"></a><h2 class="section">Bitwise operations</h2>
+<a id="lab16"></a><h2 class="section">Bitwise operations</h2>
 
 </div>
 <div class="code">

diff --git a/v9.0/stdlib/Stdlib.Bool.Bool.html b/v9.0/stdlib/Stdlib.Bool.Bool.html
@@ -89,7 +89,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab690"></a><h1 class="section">Decidability</h1>
+<a id="lab34"></a><h1 class="section">Decidability</h1>
 
 </div>
 <div class="code">
@@ -101,7 +101,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab691"></a><h1 class="section">Discrimination</h1>
+<a id="lab35"></a><h1 class="section">Discrimination</h1>
 
 </div>
 <div class="code">
@@ -137,7 +137,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab692"></a><h1 class="section">Order on booleans</h1>
+<a id="lab36"></a><h1 class="section">Order on booleans</h1>
 
 </div>
 <div class="code">
@@ -179,7 +179,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab693"></a><h1 class="section">Equality</h1>
+<a id="lab37"></a><h1 class="section">Equality</h1>
 
 </div>
 <div class="code">
@@ -222,7 +222,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab694"></a><h1 class="section">A synonym of <span class="inlinecode"><span class="id" title="keyword">if</span></span> on <span class="inlinecode"><span class="id" title="var">bool</span></span></h1>
+<a id="lab38"></a><h1 class="section">A synonym of <span class="inlinecode"><span class="id" title="keyword">if</span></span> on <span class="inlinecode"><span class="id" title="var">bool</span></span></h1>
 
 </div>
 <div class="code">
@@ -241,7 +241,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab695"></a><h1 class="section">De Morgan laws</h1>
+<a id="lab39"></a><h1 class="section">De Morgan laws</h1>
 
 </div>
 <div class="code">
@@ -256,7 +256,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab696"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">negb</span></span></h1>
+<a id="lab40"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">negb</span></span></h1>
 
 </div>
 <div class="code">
@@ -298,7 +298,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab697"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">orb</span></span></h1>
+<a id="lab41"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">orb</span></span></h1>
 
 </div>
 <div class="code">
@@ -426,7 +426,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab698"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">andb</span></span></h1>
+<a id="lab42"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">andb</span></span></h1>
 
 </div>
 <div class="code">
@@ -543,7 +543,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab699"></a><h1 class="section">Properties mixing <span class="inlinecode"><span class="id" title="var">andb</span></span> and <span class="inlinecode"><span class="id" title="var">orb</span></span></h1>
+<a id="lab43"></a><h1 class="section">Properties mixing <span class="inlinecode"><span class="id" title="var">andb</span></span> and <span class="inlinecode"><span class="id" title="var">orb</span></span></h1>
 
 <div class="paragraph"> </div>
 
@@ -593,7 +593,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab700"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">implb</span></span></h1>
+<a id="lab44"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">implb</span></span></h1>
 
 </div>
 <div class="code">
@@ -647,7 +647,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab701"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">xorb</span></span></h1>
+<a id="lab45"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">xorb</span></span></h1>
 
 <div class="paragraph"> </div>
 
@@ -809,7 +809,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab702"></a><h1 class="section">Reflection of <span class="inlinecode"><span class="id" title="var">bool</span></span> into <span class="inlinecode"><span class="id" title="keyword">Prop</span></span></h1>
+<a id="lab46"></a><h1 class="section">Reflection of <span class="inlinecode"><span class="id" title="var">bool</span></span> into <span class="inlinecode"><span class="id" title="keyword">Prop</span></span></h1>
 
 <div class="paragraph"> </div>
 
@@ -923,7 +923,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab703"></a><h1 class="section">Alternative versions of <span class="inlinecode"><span class="id" title="var">andb</span></span> and <span class="inlinecode"><span class="id" title="var">orb</span></span></h1>
+<a id="lab47"></a><h1 class="section">Alternative versions of <span class="inlinecode"><span class="id" title="var">andb</span></span> and <span class="inlinecode"><span class="id" title="var">orb</span></span></h1>
 
     with lazy behavior (for vm_compute)        
 </div>
@@ -951,7 +951,7 @@ <h1 class="libtitle">Library Stdlib.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab704"></a><h1 class="section">Reflect: a specialized inductive type for</h1>
+<a id="lab48"></a><h1 class="section">Reflect: a specialized inductive type for</h1>
 
     relating propositions and booleans,
     as popularized by the Ssreflect library.