Documentation of branch “master” at e64f7517

master/refman-stdlib/changes.html

@@ -176,15 +176,15 @@
 <h2>Unreleased changes<a class="headerlink" href="#unreleased-changes" title="Permalink to this headline">¶</a></h2>
 <div class="contents local topic" id="contents">
 <ul class="simple">
-<li><p><a class="reference internal" href="#added" id="id35">Added</a></p></li>
-<li><p><a class="reference internal" href="#changed" id="id36">Changed</a></p></li>
-<li><p><a class="reference internal" href="#renamed" id="id37">Renamed</a></p></li>
-<li><p><a class="reference internal" href="#deprecated" id="id38">Deprecated</a></p></li>
-<li><p><a class="reference internal" href="#id32" id="id39">Changed</a></p></li>
+<li><p><a class="reference internal" href="#added" id="id36">Added</a></p></li>
+<li><p><a class="reference internal" href="#changed" id="id37">Changed</a></p></li>
+<li><p><a class="reference internal" href="#renamed" id="id38">Renamed</a></p></li>
+<li><p><a class="reference internal" href="#deprecated" id="id39">Deprecated</a></p></li>
+<li><p><a class="reference internal" href="#id33" id="id40">Changed</a></p></li>
 </ul>
 </div>
 <section id="added">
-<h3><a class="toc-backref" href="#id35">Added</a><a class="headerlink" href="#added" title="Permalink to this headline">¶</a></h3>
+<h3><a class="toc-backref" href="#id36">Added</a><a class="headerlink" href="#added" title="Permalink to this headline">¶</a></h3>
 <ul class="simple">
 <li><p>in <code class="docutils literal notranslate"><span class="pre">NatInt.v</span></code></p>
 <ul>
@@ -348,10 +348,17 @@ <h3><a class="toc-backref" href="#id35">Added</a><a class="headerlink" href="#ad
 <li><p><code class="code Coq docutils literal notranslate"><span class="name"><span class="pre">EqDec</span></span></code> instance for <code class="code Coq docutils literal notranslate"><span class="name"><span class="pre">option</span></span></code></p></li>
 </ul>
 </li>
+<li><p>in <code class="docutils literal notranslate"><span class="pre">List.v</span></code></p>
+<ul>
+<li><p>lemma <code class="docutils literal notranslate"><span class="pre">length_app_comm</span></code>
+(<a class="reference external" href="https://github.com/coq/stdlib/pull/75">#75</a>,
+by Nicholas Hubbard).</p></li>
+</ul>
+</li>
 </ul>
 </section>
 <section id="changed">
-<h3><a class="toc-backref" href="#id36">Changed</a><a class="headerlink" href="#changed" title="Permalink to this headline">¶</a></h3>
+<h3><a class="toc-backref" href="#id37">Changed</a><a class="headerlink" href="#changed" title="Permalink to this headline">¶</a></h3>
 <ul class="simple">
 <li><p>Changed the requirement prefix of the standard library from <code class="docutils literal notranslate"><span class="pre">Coq</span></code>
 to <code class="docutils literal notranslate"><span class="pre">Stdlib</span></code> and made it mandatory. As a temporary measure, for
@@ -413,13 +420,13 @@ <h3><a class="toc-backref" href="#id36">Changed</a><a class="headerlink" href="#
 </ul>
 </section>
 <section id="renamed">
-<h3><a class="toc-backref" href="#id37">Renamed</a><a class="headerlink" href="#renamed" title="Permalink to this headline">¶</a></h3>
+<h3><a class="toc-backref" href="#id38">Renamed</a><a class="headerlink" href="#renamed" title="Permalink to this headline">¶</a></h3>
 </section>
 <section id="deprecated">
-<h3><a class="toc-backref" href="#id38">Deprecated</a><a class="headerlink" href="#deprecated" title="Permalink to this headline">¶</a></h3>
+<h3><a class="toc-backref" href="#id39">Deprecated</a><a class="headerlink" href="#deprecated" title="Permalink to this headline">¶</a></h3>
 </section>
-<section id="id32">
-<h3><a class="toc-backref" href="#id39">Changed</a><a class="headerlink" href="#id32" title="Permalink to this headline">¶</a></h3>
+<section id="id33">
+<h3><a class="toc-backref" href="#id40">Changed</a><a class="headerlink" href="#id33" title="Permalink to this headline">¶</a></h3>
 <ul class="simple">
 <li><p>modules <code class="code Coq docutils literal notranslate"><span class="name"><span class="pre">ZArith_Base</span></span></code> and <code class="code Coq docutils literal notranslate"><span class="name"><span class="pre">Ztac</span></span></code>,
 use <code class="code Coq docutils literal notranslate"><span class="name"><span class="pre">ZArith</span></span></code> (or <code class="code Coq docutils literal notranslate"><span class="name"><span class="pre">BinInt</span></span></code>) or <code class="code Coq docutils literal notranslate"><span class="name"><span class="pre">Lia</span></span></code> instead

master/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:      1.098s
+</span></dt><dd><span>total time:      1.100s
 
  tactic                                      local  total   calls       max
 ───────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac --------------------------------------   0.1% 100.0%       1    1.098s
-─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.6%      26    0.103s
-─&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  92.6%      26    0.103s
-─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  92.5%      26    0.103s
-─t_tauto_intuit ---------------------------   0.1%  92.4%      26    0.103s
-─&lt;Corelib.Init.Tauto.simplif&gt; -------------  58.6%  88.9%      26    0.101s
-─&lt;Corelib.Init.Tauto.is_conj&gt; -------------  23.4%  23.4%   28756    0.026s
-─lia --------------------------------------   0.1%   7.0%      28    0.052s
-─Zify.zify --------------------------------   5.0%   5.5%      54    0.051s
-─elim id ----------------------------------   3.6%   3.6%     650    0.000s
-─&lt;Corelib.Init.Tauto.axioms&gt; --------------   2.4%   3.4%       0    0.004s
+─tac --------------------------------------   0.1% 100.0%       1    1.100s
+─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.7%      26    0.070s
+─&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  92.6%      26    0.070s
+─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  92.6%      26    0.070s
+─t_tauto_intuit ---------------------------   0.1%  92.5%      26    0.070s
+─&lt;Corelib.Init.Tauto.simplif&gt; -------------  58.7%  89.0%      26    0.068s
+─&lt;Corelib.Init.Tauto.is_conj&gt; -------------  23.4%  23.4%   28756    0.031s
+─lia --------------------------------------   0.1%   7.0%      28    0.050s
+─Zify.zify --------------------------------   4.8%   5.3%      54    0.050s
+─elim id ----------------------------------   3.5%   3.5%     650    0.000s
+─&lt;Corelib.Init.Tauto.axioms&gt; --------------   2.4%   3.4%       0    0.003s
 
  tactic                                        local  total   calls       max
 ─────────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac ----------------------------------------   0.1% 100.0%       1    1.098s
- ├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.6%      26    0.103s
- │└&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  92.6%      26    0.103s
- │└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  92.5%      26    0.103s
- │└t_tauto_intuit ---------------------------   0.1%  92.4%      26    0.103s
- │ ├─&lt;Corelib.Init.Tauto.simplif&gt; -----------  58.6%  88.9%      26    0.101s
- │ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; ---------  23.4%  23.4%   28756    0.026s
- │ │ └─elim id ------------------------------   3.6%   3.6%     650    0.000s
- │ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------   2.4%   3.4%       0    0.004s
- └─lia --------------------------------------   0.1%   7.0%      28    0.052s
-  └Zify.zify --------------------------------   5.0%   5.5%      54    0.051s
+─tac ----------------------------------------   0.1% 100.0%       1    1.100s
+ ├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  92.7%      26    0.070s
+ │└&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  92.6%      26    0.070s
+ │└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  92.6%      26    0.070s
+ │└t_tauto_intuit ---------------------------   0.1%  92.5%      26    0.070s
+ │ ├─&lt;Corelib.Init.Tauto.simplif&gt; -----------  58.7%  89.0%      26    0.068s
+ │ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; ---------  23.4%  23.4%   28756    0.031s
+ │ │ └─elim id ------------------------------   3.5%   3.5%     650    0.000s
+ │ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------   2.4%   3.4%       0    0.003s
+ └─lia --------------------------------------   0.1%   7.0%      28    0.050s
+  └Zify.zify --------------------------------   4.8%   5.3%      54    0.050s
 </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.098s
+</span></dt><dd><span>total time:      1.100s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘
-─lia --   0.1%   7.0%      28    0.052s
+─lia --   0.1%   7.0%      28    0.050s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘

master/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.073 secs (0.038u,0.035s) (successful)
+</span></dt><dd><span>Finished transaction in 0.059 secs (0.032u,0.026s) (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.403 secs (0.396u,0.006s) (successful)
+</span></dt><dd><span>Finished transaction in 0.456 secs (0.449u,0.006s) (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.001 secs (0.001u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0. secs (0.u,0.s) (successful)
 1 goal
 
   H : id (fact 100)</span><span> =</span><span> fact 100

master/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">

master/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">

master/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">