Documentation of branch “master” at 3d1583e5

master/refman/proof-engine/ltac.html

@@ -3375,7 +3375,7 @@ <h3>Timing a tactic that evaluates to a term: time_constr<a class="headerlink" h
   </span><span class="coqdoc-tactic">pose</span><span> </span><span class="coqdoc-var">v</span><span>.</span><span>
 </span></dt><dd><span>Tactic evaluation (depth 1) ran for 0. secs (0.u,0.s)
 Tactic evaluation (depth 1) ran for 0. secs (0.u,0.s)
-Tactic evaluation ran for 0.001 secs (0.001u,0.s)
+Tactic evaluation ran for 0. secs (0.u,0.s)
 1 goal
 
   n := 100 : nat
@@ -4289,38 +4289,36 @@ <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.905s
+</span></dt><dd><span>total time:      2.445s
 
  tactic                                     local  total   calls       max
 ──────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac -------------------------------------   0.1% 100.0%       1    2.905s
-─&lt;Stdlib.Init.Tauto.with_uniform_flags&gt; --   0.0%  95.6%      26    0.258s
-─&lt;Stdlib.Init.Tauto.tauto_gen&gt; -----------   0.0%  95.5%      26    0.258s
-─&lt;Stdlib.Init.Tauto.tauto_intuitionistic&gt;    0.0%  95.5%      26    0.258s
-─t_tauto_intuit --------------------------   0.1%  95.4%      26    0.258s
-─&lt;Stdlib.Init.Tauto.simplif&gt; -------------  58.5%  92.3%      26    0.255s
-─&lt;Stdlib.Init.Tauto.is_conj&gt; -------------  17.9%  17.9%   28756    0.034s
-─elim id ---------------------------------  12.1%  12.1%     650    0.161s
-─&lt;Stdlib.Init.Tauto.axioms&gt; --------------   2.2%   3.1%       0    0.006s
-─split -----------------------------------   2.6%   2.6%      55    0.069s
-─intro -----------------------------------   2.0%   2.0%    1300    0.000s
+─tac -------------------------------------   0.1% 100.0%       1    2.445s
+─&lt;Stdlib.Init.Tauto.with_uniform_flags&gt; --   0.0%  93.8%      26    0.280s
+─&lt;Stdlib.Init.Tauto.tauto_gen&gt; -----------   0.0%  93.7%      26    0.280s
+─&lt;Stdlib.Init.Tauto.tauto_intuitionistic&gt;    0.0%  93.7%      26    0.280s
+─t_tauto_intuit --------------------------   0.1%  93.6%      26    0.280s
+─&lt;Stdlib.Init.Tauto.simplif&gt; -------------  55.7%  90.3%      26    0.277s
+─&lt;Stdlib.Init.Tauto.is_conj&gt; -------------  17.2%  17.2%   28756    0.000s
+─elim id ---------------------------------  13.7%  13.7%     650    0.208s
+─split -----------------------------------   4.3%   4.3%      55    0.099s
+─&lt;Stdlib.Init.Tauto.axioms&gt; --------------   2.3%   3.2%       0    0.005s
 
  tactic                                       local  total   calls       max
 ────────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac ---------------------------------------   0.1% 100.0%       1    2.905s
- ├─&lt;Stdlib.Init.Tauto.with_uniform_flags&gt; --   0.0%  95.6%      26    0.258s
- │└&lt;Stdlib.Init.Tauto.tauto_gen&gt; -----------   0.0%  95.5%      26    0.258s
- │└&lt;Stdlib.Init.Tauto.tauto_intuitionistic&gt;    0.0%  95.5%      26    0.258s
- │└t_tauto_intuit --------------------------   0.1%  95.4%      26    0.258s
- │ ├─&lt;Stdlib.Init.Tauto.simplif&gt; -----------  58.5%  92.3%      26    0.255s
- │ │ ├─&lt;Stdlib.Init.Tauto.is_conj&gt; ---------  17.9%  17.9%   28756    0.034s
- │ │ ├─elim id -----------------------------  12.1%  12.1%     650    0.161s
- │ │ └─intro -------------------------------   2.0%   2.0%    1300    0.000s
- │ └─&lt;Stdlib.Init.Tauto.axioms&gt; ------------   2.2%   3.1%       0    0.006s
- └─split -----------------------------------   2.6%   2.6%      55    0.069s
+─tac ---------------------------------------   0.1% 100.0%       1    2.445s
+ ├─&lt;Stdlib.Init.Tauto.with_uniform_flags&gt; --   0.0%  93.8%      26    0.280s
+ │└&lt;Stdlib.Init.Tauto.tauto_gen&gt; -----------   0.0%  93.7%      26    0.280s
+ │└&lt;Stdlib.Init.Tauto.tauto_intuitionistic&gt;    0.0%  93.7%      26    0.280s
+ │└t_tauto_intuit --------------------------   0.1%  93.6%      26    0.280s
+ │ ├─&lt;Stdlib.Init.Tauto.simplif&gt; -----------  55.7%  90.3%      26    0.277s
+ │ │ ├─&lt;Stdlib.Init.Tauto.is_conj&gt; ---------  17.2%  17.2%   28756    0.000s
+ │ │ └─elim id -----------------------------  13.7%  13.7%     650    0.208s
+ │ └─&lt;Stdlib.Init.Tauto.axioms&gt; ------------   2.3%   3.2%       0    0.005s
+ └─split -----------------------------------   4.3%   4.3%      55    0.099s
 </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.905s
+</span></dt><dd><span>total time:      2.445s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘

master/refman/proofs/writing-proofs/equality.html

@@ -2633,15 +2633,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.211 secs (0.188u,0.022s) (successful)
+</span></dt><dd><span>Finished transaction in 0.22 secs (0.169u,0.05s) (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 1.502 secs (1.502u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 1.191 secs (1.19u,0.s) (successful)
 1 goal
 
   H : id (fact 8)</span><span> =</span><span> fact 8
@@ -2669,7 +2669,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.003 secs (0.003u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0.001 secs (0.001u,0.s) (successful)
 1 goal
 
   H : id (fact 100)</span><span> =</span><span> fact 100
@@ -2704,7 +2704,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.006 secs (0.006u,0.s) (successful)
+</span></dt><dd><span>Finished transaction in 0.001 secs (0.001u,0.s) (successful)
 1 goal
 
   H : id (fact 100)</span><span> =</span><span> fact 100

master/stdlib/Stdlib.Arith.Arith_base.html

@@ -58,7 +58,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="lab238"></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 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="lab239"></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

@@ -56,7 +56,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="lab237"></a><h1 class="section">Propositional equality</h1>
 
 </div>
 <div class="code">

master/stdlib/Stdlib.Arith.PeanoNat.html

@@ -149,7 +149,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="lab222"></a><h2 class="section">Remaining constants not defined in Stdlib.Init.Nat</h2>
 
 <div class="paragraph"> </div>
 
@@ -167,7 +167,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="lab223"></a><h2 class="section">Basic specifications : pred add sub mul</h2>
 
 </div>
 <div class="code">
@@ -209,7 +209,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="lab224"></a><h2 class="section">Boolean comparisons</h2>
 
 </div>
 <div class="code">
@@ -241,7 +241,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="lab225"></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 Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab6"></a><h2 class="section">Ternary comparison</h2>
+<a id="lab226"></a><h2 class="section">Ternary comparison</h2>
 
 <div class="paragraph"> </div>
 
@@ -282,7 +282,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="lab227"></a><h2 class="section">Minimum, maximum</h2>
 
 </div>
 <div class="code">
@@ -332,7 +332,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab8"></a><h2 class="section">Power</h2>
+<a id="lab228"></a><h2 class="section">Power</h2>
 
 </div>
 <div class="code">
@@ -350,7 +350,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab9"></a><h2 class="section">Square</h2>
+<a id="lab229"></a><h2 class="section">Square</h2>
 
 </div>
 <div class="code">
@@ -362,7 +362,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab10"></a><h2 class="section">Parity</h2>
+<a id="lab230"></a><h2 class="section">Parity</h2>
 
 </div>
 <div class="code">
@@ -406,7 +406,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab11"></a><h2 class="section">Division</h2>
+<a id="lab231"></a><h2 class="section">Division</h2>
 
 </div>
 <div class="code">
@@ -435,7 +435,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="lab232"></a><h2 class="section">Square root</h2>
 
 </div>
 <div class="code">
@@ -459,7 +459,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab13"></a><h2 class="section">Logarithm</h2>
+<a id="lab233"></a><h2 class="section">Logarithm</h2>
 
 </div>
 <div class="code">
@@ -481,7 +481,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="lab234"></a><h2 class="section">Properties of <span class="inlinecode"><span class="id" title="var">iter</span></span></h2>
 
 </div>
 <div class="code">
@@ -533,7 +533,7 @@ <h1 class="libtitle">Library Stdlib.Arith.PeanoNat</h1>
 </div>
 
 <div class="doc">
-<a id="lab15"></a><h2 class="section">Gcd</h2>
+<a id="lab235"></a><h2 class="section">Gcd</h2>
 
 </div>
 <div class="code">
@@ -561,7 +561,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="lab236"></a><h2 class="section">Bitwise operations</h2>
 
 </div>
 <div class="code">