Documentation of branch “master” at 2d41f821

coq · Jan 12, 2024 · 145f3cd · 145f3cd
1 parent 1b5582e
commit 145f3cd
Show file tree

Hide file tree

Showing 263 changed files with 1,395 additions and 1,266 deletions.
diff --git a/master/refman/.doctrees/addendum/extraction.doctree b/master/refman/.doctrees/addendum/extraction.doctree
diff --git a/master/refman/.doctrees/addendum/generalized-rewriting.doctree b/master/refman/.doctrees/addendum/generalized-rewriting.doctree
diff --git a/master/refman/.doctrees/addendum/implicit-coercions.doctree b/master/refman/.doctrees/addendum/implicit-coercions.doctree
diff --git a/master/refman/.doctrees/addendum/micromega.doctree b/master/refman/.doctrees/addendum/micromega.doctree
diff --git a/master/refman/.doctrees/addendum/miscellaneous-extensions.doctree b/master/refman/.doctrees/addendum/miscellaneous-extensions.doctree
diff --git a/master/refman/.doctrees/addendum/program.doctree b/master/refman/.doctrees/addendum/program.doctree
diff --git a/master/refman/.doctrees/addendum/ring.doctree b/master/refman/.doctrees/addendum/ring.doctree
diff --git a/master/refman/.doctrees/addendum/sprop.doctree b/master/refman/.doctrees/addendum/sprop.doctree
diff --git a/master/refman/.doctrees/addendum/type-classes.doctree b/master/refman/.doctrees/addendum/type-classes.doctree
diff --git a/master/refman/.doctrees/addendum/universe-polymorphism.doctree b/master/refman/.doctrees/addendum/universe-polymorphism.doctree
diff --git a/master/refman/.doctrees/changes.doctree b/master/refman/.doctrees/changes.doctree
diff --git a/master/refman/.doctrees/environment.pickle b/master/refman/.doctrees/environment.pickle
diff --git a/master/refman/.doctrees/language/cic.doctree b/master/refman/.doctrees/language/cic.doctree
diff --git a/master/refman/.doctrees/language/coq-library.doctree b/master/refman/.doctrees/language/coq-library.doctree
diff --git a/master/refman/.doctrees/language/core/assumptions.doctree b/master/refman/.doctrees/language/core/assumptions.doctree
diff --git a/master/refman/.doctrees/language/core/basic.doctree b/master/refman/.doctrees/language/core/basic.doctree
diff --git a/master/refman/.doctrees/language/core/coinductive.doctree b/master/refman/.doctrees/language/core/coinductive.doctree
diff --git a/master/refman/.doctrees/language/core/conversion.doctree b/master/refman/.doctrees/language/core/conversion.doctree
diff --git a/master/refman/.doctrees/language/core/inductive.doctree b/master/refman/.doctrees/language/core/inductive.doctree
diff --git a/master/refman/.doctrees/language/core/modules.doctree b/master/refman/.doctrees/language/core/modules.doctree
diff --git a/master/refman/.doctrees/language/core/primitive.doctree b/master/refman/.doctrees/language/core/primitive.doctree
diff --git a/master/refman/.doctrees/language/core/records.doctree b/master/refman/.doctrees/language/core/records.doctree
diff --git a/master/refman/.doctrees/language/core/sections.doctree b/master/refman/.doctrees/language/core/sections.doctree
diff --git a/master/refman/.doctrees/language/core/variants.doctree b/master/refman/.doctrees/language/core/variants.doctree
diff --git a/master/refman/.doctrees/language/extensions/arguments-command.doctree b/master/refman/.doctrees/language/extensions/arguments-command.doctree
diff --git a/master/refman/.doctrees/language/extensions/canonical.doctree b/master/refman/.doctrees/language/extensions/canonical.doctree
diff --git a/master/refman/.doctrees/language/extensions/evars.doctree b/master/refman/.doctrees/language/extensions/evars.doctree
diff --git a/master/refman/.doctrees/language/extensions/implicit-arguments.doctree b/master/refman/.doctrees/language/extensions/implicit-arguments.doctree
diff --git a/master/refman/.doctrees/language/extensions/match.doctree b/master/refman/.doctrees/language/extensions/match.doctree
diff --git a/master/refman/.doctrees/practical-tools/coq-commands.doctree b/master/refman/.doctrees/practical-tools/coq-commands.doctree
diff --git a/master/refman/.doctrees/practical-tools/coqide.doctree b/master/refman/.doctrees/practical-tools/coqide.doctree
diff --git a/master/refman/.doctrees/proof-engine/ltac.doctree b/master/refman/.doctrees/proof-engine/ltac.doctree
diff --git a/master/refman/.doctrees/proof-engine/ltac2.doctree b/master/refman/.doctrees/proof-engine/ltac2.doctree
diff --git a/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree b/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree
diff --git a/master/refman/.doctrees/proof-engine/tactics.doctree b/master/refman/.doctrees/proof-engine/tactics.doctree
diff --git a/master/refman/.doctrees/proof-engine/vernacular-commands.doctree b/master/refman/.doctrees/proof-engine/vernacular-commands.doctree
diff --git a/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree b/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree
diff --git a/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree b/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree
diff --git a/master/refman/.doctrees/proofs/writing-proofs/equality.doctree b/master/refman/.doctrees/proofs/writing-proofs/equality.doctree
diff --git a/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree b/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree
diff --git a/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree b/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree
diff --git a/master/refman/.doctrees/user-extensions/syntax-extensions.doctree b/master/refman/.doctrees/user-extensions/syntax-extensions.doctree
diff --git a/master/refman/.doctrees/using/libraries/funind.doctree b/master/refman/.doctrees/using/libraries/funind.doctree
diff --git a/master/refman/.doctrees/using/libraries/writing.doctree b/master/refman/.doctrees/using/libraries/writing.doctree
diff --git a/master/refman/proof-engine/ltac.html b/master/refman/proof-engine/ltac.html
@@ -4241,37 +4241,37 @@ <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:      2.651s
+</span></dt><dd><span>total time:      2.992s
 
  tactic                                   local  total   calls       max 
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac -----------------------------------   0.1% 100.0%       1    2.651s
-─&lt;Coq.Init.Tauto.with_uniform_flags&gt; ---   0.0%  95.8%      26    0.269s
-─&lt;Coq.Init.Tauto.tauto_gen&gt; ------------   0.0%  95.8%      26    0.269s
-─&lt;Coq.Init.Tauto.tauto_intuitionistic&gt; -   0.0%  95.7%      26    0.269s
-─t_tauto_intuit ------------------------   0.0%  95.6%      26    0.269s
-─&lt;Coq.Init.Tauto.simplif&gt; --------------  59.4%  92.7%      26    0.266s
-─&lt;Coq.Init.Tauto.is_conj&gt; --------------  24.7%  24.7%   28756    0.178s
-─elim id -------------------------------   5.3%   5.3%     650    0.003s
+─tac -----------------------------------   0.1% 100.0%       1    2.992s
+─&lt;Coq.Init.Tauto.with_uniform_flags&gt; ---   0.0%  95.8%      26    0.274s
+─&lt;Coq.Init.Tauto.tauto_gen&gt; ------------   0.0%  95.8%      26    0.274s
+─&lt;Coq.Init.Tauto.tauto_intuitionistic&gt; -   0.0%  95.7%      26    0.273s
+─t_tauto_intuit ------------------------   0.0%  95.6%      26    0.273s
+─&lt;Coq.Init.Tauto.simplif&gt; --------------  60.7%  92.7%      26    0.270s
+─&lt;Coq.Init.Tauto.is_conj&gt; --------------  24.1%  24.1%   28756    0.180s
+─elim id -------------------------------   4.7%   4.7%     650    0.003s
 ─&lt;Coq.Init.Tauto.axioms&gt; ---------------   2.1%   2.9%       0    0.004s
-─split ---------------------------------   2.4%   2.4%      55    0.060s
+─split ---------------------------------   2.4%   2.4%      55    0.069s
 
  tactic                                   local  total   calls       max 
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac -----------------------------------   0.1% 100.0%       1    2.651s
- ├─&lt;Coq.Init.Tauto.with_uniform_flags&gt; -   0.0%  95.8%      26    0.269s
- │└&lt;Coq.Init.Tauto.tauto_gen&gt; ----------   0.0%  95.8%      26    0.269s
- │└&lt;Coq.Init.Tauto.tauto_intuitionistic&gt;   0.0%  95.7%      26    0.269s
- │└t_tauto_intuit ----------------------   0.0%  95.6%      26    0.269s
- │ ├─&lt;Coq.Init.Tauto.simplif&gt; ----------  59.4%  92.7%      26    0.266s
- │ │ ├─&lt;Coq.Init.Tauto.is_conj&gt; --------  24.7%  24.7%   28756    0.178s
- │ │ └─elim id -------------------------   5.3%   5.3%     650    0.003s
+─tac -----------------------------------   0.1% 100.0%       1    2.992s
+ ├─&lt;Coq.Init.Tauto.with_uniform_flags&gt; -   0.0%  95.8%      26    0.274s
+ │└&lt;Coq.Init.Tauto.tauto_gen&gt; ----------   0.0%  95.8%      26    0.274s
+ │└&lt;Coq.Init.Tauto.tauto_intuitionistic&gt;   0.0%  95.7%      26    0.273s
+ │└t_tauto_intuit ----------------------   0.0%  95.6%      26    0.273s
+ │ ├─&lt;Coq.Init.Tauto.simplif&gt; ----------  60.7%  92.7%      26    0.270s
+ │ │ ├─&lt;Coq.Init.Tauto.is_conj&gt; --------  24.1%  24.1%   28756    0.180s
+ │ │ └─elim id -------------------------   4.7%   4.7%     650    0.003s
  │ └─&lt;Coq.Init.Tauto.axioms&gt; -----------   2.1%   2.9%       0    0.004s
- └─split -------------------------------   2.4%   2.4%      55    0.060s
+ └─split -------------------------------   2.4%   2.4%      55    0.069s
 
 </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:      2.651s
+</span></dt><dd><span>total time:      2.992s
 
  tactic                                   local  total   calls       max 
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘

diff --git a/master/refman/proofs/writing-proofs/equality.html b/master/refman/proofs/writing-proofs/equality.html
@@ -2554,15 +2554,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.117 secs (0.089u,0.027s) (successful)
+</span></dt><dd><span>Finished transaction in 0.207 secs (0.184u,0.022s) (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.857 secs (0.857u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 1.532 secs (1.532u,0.s) (successful)
 1 goal
 
   H : id (fact 8)</span><span> =</span><span> fact 8
@@ -2590,7 +2590,7 @@ <h3>Computing in a term: eval and Eval<a class="headerlink" href="#computing-in-
 Timeout!
 </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> 100) = </span><span class="coqdoc-var">fact</span><span> 100) </span><span class="coqdoc-tactic">by</span><span> </span><span class="coqdoc-var">with_strategy</span><span> -1 [</span><span class="coqdoc-var">id</span><span>] </span><span class="coqdoc-tactic">reflexivity</span><span>.</span><span>
-</span></dt><dd><span>Finished transaction in 0.001 secs (0.001u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0.002 secs (0.002u,0.s) (successful)
 1 goal
 
   H : id (fact 100)</span><span> =</span><span> fact 100
@@ -2625,7 +2625,7 @@ <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> 100) = </span><span class="coqdoc-var">fact</span><span> 100) </span><span class="coqdoc-tactic">by</span><span> </span><span class="coqdoc-var">with_strategy</span><span> -1 [</span><span class="coqdoc-var">id</span><span>] </span><span class="coqdoc-tactic">abstract</span><span> </span><span class="coqdoc-tactic">reflexivity</span><span>.</span><span>
-</span></dt><dd><span>Finished transaction in 0.002 secs (0.002u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0.003 secs (0.003u,0.s) (successful)
 1 goal
 
   H : id (fact 100)</span><span> =</span><span> fact 100

diff --git a/master/refman/searchindex.js b/master/refman/searchindex.js
diff --git a/master/stdlib/Coq.Arith.Arith_base.html b/master/stdlib/Coq.Arith.Arith_base.html
@@ -58,7 +58,7 @@ <h1 class="libtitle">Library Coq.Arith.Arith_base</h1>
 </div>
 
 <div class="doc">
-<a id="lab17"></a><h1 class="section"><span class="inlinecode"><span class="id" title="var">arith</span></span> hint database</h1>
+<a id="lab631"></a><h1 class="section"><span class="inlinecode"><span class="id" title="var">arith</span></span> hint database</h1>
 
 </div>
 <div class="code">
@@ -80,7 +80,7 @@ <h1 class="libtitle">Library Coq.Arith.Arith_base</h1>
 </div>
 
 <div class="doc">
-<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>
+<a id="lab632"></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/master/stdlib/Coq.Arith.EqNat.html b/master/stdlib/Coq.Arith.EqNat.html
@@ -56,7 +56,7 @@ <h1 class="libtitle">Library Coq.Arith.EqNat</h1>
 Equality on natural numbers 
 <div class="paragraph"> </div>
 
-<a id="lab1"></a><h1 class="section">Propositional equality</h1>
+<a id="lab615"></a><h1 class="section">Propositional equality</h1>
 
 </div>
 <div class="code">

diff --git a/master/stdlib/Coq.Arith.PeanoNat.html b/master/stdlib/Coq.Arith.PeanoNat.html
@@ -149,7 +149,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab2"></a><h2 class="section">Remaining constants not defined in Coq.Init.Nat</h2>
+<a id="lab616"></a><h2 class="section">Remaining constants not defined in Coq.Init.Nat</h2>
 
 <div class="paragraph"> </div>
 
@@ -167,7 +167,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab3"></a><h2 class="section">Basic specifications : pred add sub mul</h2>
+<a id="lab617"></a><h2 class="section">Basic specifications : pred add sub mul</h2>
 
 </div>
 <div class="code">
@@ -209,7 +209,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab4"></a><h2 class="section">Boolean comparisons</h2>
+<a id="lab618"></a><h2 class="section">Boolean comparisons</h2>
 
 </div>
 <div class="code">
@@ -241,7 +241,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab5"></a><h2 class="section">Decidability of equality over <span class="inlinecode"><span class="id" title="var">nat</span></span>.</h2>
+<a id="lab619"></a><h2 class="section">Decidability of equality over <span class="inlinecode"><span class="id" title="var">nat</span></span>.</h2>
 
 </div>
 <div class="code">
@@ -253,7 +253,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab6"></a><h2 class="section">Ternary comparison</h2>
+<a id="lab620"></a><h2 class="section">Ternary comparison</h2>
 
 <div class="paragraph"> </div>
 
@@ -282,7 +282,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab7"></a><h2 class="section">Minimum, maximum</h2>
+<a id="lab621"></a><h2 class="section">Minimum, maximum</h2>
 
 </div>
 <div class="code">
@@ -328,7 +328,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab8"></a><h2 class="section">Power</h2>
+<a id="lab622"></a><h2 class="section">Power</h2>
 
 </div>
 <div class="code">
@@ -346,7 +346,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab9"></a><h2 class="section">Square</h2>
+<a id="lab623"></a><h2 class="section">Square</h2>
 
 </div>
 <div class="code">
@@ -358,7 +358,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab10"></a><h2 class="section">Parity</h2>
+<a id="lab624"></a><h2 class="section">Parity</h2>
 
 </div>
 <div class="code">
@@ -402,7 +402,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab11"></a><h2 class="section">Division</h2>
+<a id="lab625"></a><h2 class="section">Division</h2>
 
 </div>
 <div class="code">
@@ -431,7 +431,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab12"></a><h2 class="section">Square root</h2>
+<a id="lab626"></a><h2 class="section">Square root</h2>
 
 </div>
 <div class="code">
@@ -455,7 +455,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab13"></a><h2 class="section">Logarithm</h2>
+<a id="lab627"></a><h2 class="section">Logarithm</h2>
 
 </div>
 <div class="code">
@@ -477,7 +477,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab14"></a><h2 class="section">Properties of <span class="inlinecode"><span class="id" title="var">iter</span></span></h2>
+<a id="lab628"></a><h2 class="section">Properties of <span class="inlinecode"><span class="id" title="var">iter</span></span></h2>
 
 </div>
 <div class="code">
@@ -529,7 +529,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab15"></a><h2 class="section">Gcd</h2>
+<a id="lab629"></a><h2 class="section">Gcd</h2>
 
 </div>
 <div class="code">
@@ -557,7 +557,7 @@ <h1 class="libtitle">Library Coq.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab16"></a><h2 class="section">Bitwise operations</h2>
+<a id="lab630"></a><h2 class="section">Bitwise operations</h2>
 
 </div>
 <div class="code">

diff --git a/master/stdlib/Coq.Bool.Bool.html b/master/stdlib/Coq.Bool.Bool.html
@@ -90,7 +90,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab34"></a><h1 class="section">Decidability</h1>
+<a id="lab423"></a><h1 class="section">Decidability</h1>
 
 </div>
 <div class="code">
@@ -102,7 +102,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab35"></a><h1 class="section">Discrimination</h1>
+<a id="lab424"></a><h1 class="section">Discrimination</h1>
 
 </div>
 <div class="code">
@@ -138,7 +138,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab36"></a><h1 class="section">Order on booleans</h1>
+<a id="lab425"></a><h1 class="section">Order on booleans</h1>
 
 </div>
 <div class="code">
@@ -180,7 +180,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab37"></a><h1 class="section">Equality</h1>
+<a id="lab426"></a><h1 class="section">Equality</h1>
 
 </div>
 <div class="code">
@@ -223,7 +223,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<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>
+<a id="lab427"></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">
@@ -242,7 +242,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab39"></a><h1 class="section">De Morgan laws</h1>
+<a id="lab428"></a><h1 class="section">De Morgan laws</h1>
 
 </div>
 <div class="code">
@@ -257,7 +257,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab40"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">negb</span></span></h1>
+<a id="lab429"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">negb</span></span></h1>
 
 </div>
 <div class="code">
@@ -299,7 +299,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab41"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">orb</span></span></h1>
+<a id="lab430"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">orb</span></span></h1>
 
 </div>
 <div class="code">
@@ -427,7 +427,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab42"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">andb</span></span></h1>
+<a id="lab431"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">andb</span></span></h1>
 
 </div>
 <div class="code">
@@ -544,7 +544,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<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>
+<a id="lab432"></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>
 
@@ -594,7 +594,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab44"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">implb</span></span></h1>
+<a id="lab433"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">implb</span></span></h1>
 
 </div>
 <div class="code">
@@ -648,7 +648,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab45"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">xorb</span></span></h1>
+<a id="lab434"></a><h1 class="section">Properties of <span class="inlinecode"><span class="id" title="var">xorb</span></span></h1>
 
 <div class="paragraph"> </div>
 
@@ -810,7 +810,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<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>
+<a id="lab435"></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>
 
@@ -924,7 +924,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<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>
+<a id="lab436"></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>
@@ -952,7 +952,7 @@ <h1 class="libtitle">Library Coq.Bool.Bool</h1>
 </div>
 
 <div class="doc">
-<a id="lab48"></a><h1 class="section">Reflect: a specialized inductive type for</h1>
+<a id="lab437"></a><h1 class="section">Reflect: a specialized inductive type for</h1>
 
     relating propositions and booleans,
     as popularized by the Ssreflect library.