Documentation of branch “v9.0” at 3d0c00bb

v9.0/refman/_static/coqdoc.css

@@ -70,3 +70,50 @@
 .smallcaps {
     font-variant: small-caps;
 }
+
+
+:root {
+    --refman-custom-primary-blue: #260086;
+    --refman-custom-primary-blue-2: #040b92;
+    --refman-custom-secondary-orange: #ff540a;
+    --refman-custom-secondary-orange-2: #ffe9df;
+}
+
+.btn-info:hover, a:hover, a.wy-text-info:hover {
+    color: var(--refman-custom-primary-blue-2) !important
+}
+
+.wy-menu-vertical header, .wy-menu-vertical p.caption, .rst-content .wy-alert-neutral.admonition-todo a, .rst-content .wy-alert-neutral.admonition a, .rst-content .wy-alert-neutral.attention a, .rst-content .wy-alert-neutral.caution a, .rst-content .wy-alert-neutral.danger a, .rst-content .wy-alert-neutral.error a, .rst-content .wy-alert-neutral.hint a, .rst-content .wy-alert-neutral.important a, .rst-content .wy-alert-neutral.note a, .rst-content .wy-alert-neutral.seealso a, .rst-content .wy-alert-neutral.tip a, .rst-content .wy-alert-neutral.warning a, .wy-alert.wy-alert-neutral a, a, .wy-text-info, .btn-link, .wy-inline-validate.wy-inline-validate-info .wy-input-context, .wy-nav .wy-menu-vertical header, .rst-versions a, .rst-content a code, .rst-content a tt, html.writer-html4 .rst-content dl:not(.docutils)>dt, html.writer-html5 .rst-content dl[class]:not(.option-list):not(.field-list):not(.footnote):not(.glossary):not(.simple)>dt, html.writer-html4 .rst-content dl:not(.docutils)>dt:before, html.writer-html5 .rst-content dl[class]:not(.option-list):not(.field-list):not(.footnote):not(.glossary):not(.simple)>dt:before {
+    color: var(--refman-custom-primary-blue) !important
+}
+
+.rst-content .note .admonition-title,.rst-content .note .wy-alert-title,.rst-content .seealso .admonition-title,.rst-content .seealso .wy-alert-title,.rst-content .wy-alert-info.admonition-todo .admonition-title,.rst-content .wy-alert-info.admonition-todo .wy-alert-title,.rst-content .wy-alert-info.admonition .admonition-title,.rst-content .wy-alert-info.admonition .wy-alert-title,.rst-content .wy-alert-info.attention .admonition-title,.rst-content .wy-alert-info.attention .wy-alert-title,.rst-content .wy-alert-info.caution .admonition-title,.rst-content .wy-alert-info.caution .wy-alert-title,.rst-content .wy-alert-info.danger .admonition-title,.rst-content .wy-alert-info.danger .wy-alert-title,.rst-content .wy-alert-info.error .admonition-title,.rst-content .wy-alert-info.error .wy-alert-title,.rst-content .wy-alert-info.hint .admonition-title,.rst-content .wy-alert-info.hint .wy-alert-title,.rst-content .wy-alert-info.important .admonition-title,.rst-content .wy-alert-info.important .wy-alert-title,.rst-content .wy-alert-info.tip .admonition-title,.rst-content .wy-alert-info.tip .wy-alert-title,.rst-content .wy-alert-info.warning .admonition-title,.rst-content .wy-alert-info.warning .wy-alert-title,.rst-content .wy-alert.wy-alert-info .admonition-title,.wy-alert.wy-alert-info .rst-content .admonition-title,.wy-alert.wy-alert-info .wy-alert-title {
+    background: var(--refman-custom-primary-blue) !important
+}
+
+html.writer-html4 .rst-content dl:not(.docutils)>dt,html.writer-html5 .rst-content dl[class]:not(.option-list):not(.field-list):not(.footnote):not(.glossary):not(.simple)>dt {
+    background: var(--refman-custom-secondary-orange-2) !important;
+    color: var(--refman-custom-primary-blue) !important;
+    border-top: 3px solid var(--refman-custom-secondary-orange) !important;
+}
+
+.wy-tray-container li.wy-tray-item-info, .btn-info, .wy-menu-vertical a:active, .wy-side-nav-search, .wy-dropdown-menu>dd>a:hover, .wy-dropdown.wy-dropdown-bubble .wy-dropdown-menu a:hover, .wy-side-nav-search img, .wy-nav .wy-menu-vertical a:hover, .wy-nav-top, .wy-nav-top img {
+    background-color: var(--refman-custom-secondary-orange) !important
+}
+
+.wy-side-nav-search input[type=text] {
+    border-color: var(--refman-custom-primary-blue-2) !important
+}
+
+.rst-versions, .wy-nav-side {
+    background: #dedede !important;
+}
+
+.wy-side-nav-search>div.version {
+    color: #dedede !important;
+}
+
+.wy-menu-vertical a:hover {
+    background-color: #494949 !important;
+    color: #dedede !important;
+}

v9.0/refman/proof-engine/ltac.html

@@ -4287,42 +4287,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:      0.912s
+</span></dt><dd><span>total time:      2.043s
 
  tactic                                      local  total   calls       max
 ───────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac --------------------------------------   0.1% 100.0%       1    0.912s
-─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.0%      26    0.066s
-─&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  91.9%      26    0.066s
-─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  91.8%      26    0.066s
-─t_tauto_intuit ---------------------------   0.1%  91.7%      26    0.066s
-─&lt;Corelib.Init.Tauto.simplif&gt; -------------  57.8%  88.2%      26    0.065s
-─&lt;Corelib.Init.Tauto.is_conj&gt; -------------  24.2%  24.2%   28756    0.009s
-─lia --------------------------------------   0.1%   7.8%      28    0.053s
-─Zify.zify --------------------------------   6.0%   6.5%      54    0.052s
-─&lt;Corelib.Init.Tauto.axioms&gt; --------------   2.4%   3.5%       0    0.003s
-─elim id ----------------------------------   2.9%   2.9%     650    0.000s
+─tac --------------------------------------   0.2% 100.0%       1    2.043s
+─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.9%      26    0.188s
+─&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  92.9%      26    0.188s
+─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.0%  92.8%      26    0.188s
+─t_tauto_intuit ---------------------------   0.1%  92.7%      26    0.188s
+─&lt;Corelib.Init.Tauto.simplif&gt; -------------  63.4%  89.3%      26    0.186s
+─&lt;Corelib.Init.Tauto.is_conj&gt; -------------  19.2%  19.2%   28756    0.016s
+─lia --------------------------------------   0.1%   6.6%      28    0.087s
+─Zify.zify --------------------------------   4.5%   5.1%      54    0.087s
+─elim id ----------------------------------   3.4%   3.4%     650    0.000s
+─&lt;Corelib.Init.Tauto.axioms&gt; --------------   2.5%   3.4%       0    0.007s
 
  tactic                                        local  total   calls       max
 ─────────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac ----------------------------------------   0.1% 100.0%       1    0.912s
- ├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  91.9%      26    0.066s
- │└&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  91.9%      26    0.066s
- │└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  91.8%      26    0.066s
- │└t_tauto_intuit ---------------------------   0.1%  91.7%      26    0.066s
- │ ├─&lt;Corelib.Init.Tauto.simplif&gt; -----------  57.8%  88.2%      26    0.065s
- │ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; ---------  24.2%  24.2%   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.8%      28    0.053s
-  └Zify.zify --------------------------------   6.0%   6.5%      54    0.052s
+─tac ----------------------------------------   0.2% 100.0%       1    2.043s
+ ├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.9%      26    0.188s
+ │└&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  92.9%      26    0.188s
+ │└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.0%  92.8%      26    0.188s
+ │└t_tauto_intuit ---------------------------   0.1%  92.7%      26    0.188s
+ │ ├─&lt;Corelib.Init.Tauto.simplif&gt; -----------  63.4%  89.3%      26    0.186s
+ │ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; ---------  19.2%  19.2%   28756    0.016s
+ │ │ └─elim id ------------------------------   3.4%   3.4%     650    0.000s
+ │ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------   2.5%   3.4%       0    0.007s
+ └─lia --------------------------------------   0.1%   6.6%      28    0.087s
+  └Zify.zify --------------------------------   4.5%   5.1%      54    0.087s
 </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:      0.912s
+</span></dt><dd><span>total time:      2.043s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘
-─lia --   0.1%   7.8%      28    0.053s
+─lia --   0.1%   6.6%      28    0.087s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘

v9.0/refman/proofs/writing-proofs/equality.html

@@ -2641,15 +2641,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.056 secs (0.051u,0.005s) (successful)
+</span></dt><dd><span>Finished transaction in 0.168 secs (0.074u,0.094s) (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.275 secs (0.275u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0.965 secs (0.965u,0.s) (successful)
 1 goal
 
   H : id (fact 8)</span><span> =</span><span> fact 8
@@ -2677,7 +2677,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. secs (0.u,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
@@ -2712,7 +2712,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.001 secs (0.001u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0.004 secs (0.004u,0.s) (successful)
 1 goal
 
   H : id (fact 100)</span><span> =</span><span> fact 100
@@ -2723,7 +2723,7 @@ <h3>Computing in a term: eval and Eval<a class="headerlink" href="#computing-in-
 </span></dt><dd><span>No more goals.
 </span></dd>
 <dt><span></span><span class="coqdoc-keyword">Time</span><span> </span><span class="coqdoc-keyword">Defined</span><span>.</span><span>
-</span></dt><dd><span>Finished transaction in 0. secs (0.u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0.001 secs (0.001u,0.s) (successful)
 </span></dd>
 </dl>
 </div>

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="lab17"></a><h1 class="section"><span class="inlinecode"><span class="id" title="var">arith</span></span> hint database</h1>
+<a id="lab1"></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="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="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>
 
 </div>
 <div class="code">

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="lab1"></a><h1 class="section">Propositional equality</h1>
+<a id="lab18"></a><h1 class="section">Propositional equality</h1>
 
 </div>
 <div class="code">

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="lab2"></a><h2 class="section">Remaining constants not defined in Stdlib.Init.Nat</h2>
+<a id="lab3"></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="lab3"></a><h2 class="section">Basic specifications : pred add sub mul</h2>
+<a id="lab4"></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="lab4"></a><h2 class="section">Boolean comparisons</h2>
+<a id="lab5"></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="lab5"></a><h2 class="section">Decidability of equality over <span class="inlinecode"><span class="id" title="var">nat</span></span>.</h2>
+<a id="lab6"></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="lab6"></a><h2 class="section">Ternary comparison</h2>
+<a id="lab7"></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="lab7"></a><h2 class="section">Minimum, maximum</h2>
+<a id="lab8"></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="lab8"></a><h2 class="section">Power</h2>
+<a id="lab9"></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="lab9"></a><h2 class="section">Square</h2>
+<a id="lab10"></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="lab10"></a><h2 class="section">Parity</h2>
+<a id="lab11"></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="lab11"></a><h2 class="section">Division</h2>
+<a id="lab12"></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="lab12"></a><h2 class="section">Square root</h2>
+<a id="lab13"></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="lab13"></a><h2 class="section">Logarithm</h2>
+<a id="lab14"></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="lab14"></a><h2 class="section">Properties of <span class="inlinecode"><span class="id" title="var">iter</span></span></h2>
+<a id="lab15"></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="lab15"></a><h2 class="section">Gcd</h2>
+<a id="lab16"></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="lab16"></a><h2 class="section">Bitwise operations</h2>
+<a id="lab17"></a><h2 class="section">Bitwise operations</h2>
 
 </div>
 <div class="code">