Documentation of branch “master” at 781308dd

Author: coqbot

master/refman/.doctrees/addendum/extraction.doctree

@@ -4285,42 +4285,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.166s
+</span></dt><dd><span>total time:      1.242s
 
  tactic                                      local  total   calls       max
 ───────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac --------------------------------------   0.1% 100.0%       1    1.166s
-─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  97.2%      26    0.097s
-─&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  97.2%      26    0.097s
-─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  97.1%      26    0.097s
-─t_tauto_intuit ---------------------------   0.1%  97.0%      26    0.097s
-─&lt;Corelib.Init.Tauto.simplif&gt; -------------  62.2%  93.7%      26    0.095s
-─&lt;Corelib.Init.Tauto.is_conj&gt; -------------  20.1%  20.1%   28756    0.003s
-─clear (hyp_list) -------------------------   4.9%   4.9%     650    0.051s
-─elim id ----------------------------------   3.6%   3.6%     650    0.003s
-─&lt;Corelib.Init.Tauto.axioms&gt; --------------   2.3%   3.3%       0    0.003s
-─lia --------------------------------------   0.1%   2.4%      28    0.014s
+─tac --------------------------------------   0.1% 100.0%       1    1.242s
+─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  97.6%      26    0.094s
+─&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  97.5%      26    0.094s
+─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  97.5%      26    0.094s
+─t_tauto_intuit ---------------------------   0.1%  97.4%      26    0.094s
+─&lt;Corelib.Init.Tauto.simplif&gt; -------------  61.8%  93.7%      26    0.092s
+─&lt;Corelib.Init.Tauto.is_conj&gt; -------------  20.7%  20.7%   28756    0.003s
+─clear (hyp_list) -------------------------   4.4%   4.4%     650    0.048s
+─elim id ----------------------------------   4.0%   4.0%     650    0.003s
+─&lt;Corelib.Init.Tauto.axioms&gt; --------------   2.6%   3.6%       0    0.005s
+─lia --------------------------------------   0.1%   2.1%      28    0.012s
 
  tactic                                        local  total   calls       max
 ─────────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac ----------------------------------------   0.1% 100.0%       1    1.166s
- ├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  97.2%      26    0.097s
- │└&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  97.2%      26    0.097s
- │└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  97.1%      26    0.097s
- │└t_tauto_intuit ---------------------------   0.1%  97.0%      26    0.097s
- │ ├─&lt;Corelib.Init.Tauto.simplif&gt; -----------  62.2%  93.7%      26    0.095s
- │ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; ---------  20.1%  20.1%   28756    0.003s
- │ │ ├─clear (hyp_list) ---------------------   4.9%   4.9%     650    0.051s
- │ │ └─elim id ------------------------------   3.6%   3.6%     650    0.003s
- │ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------   2.3%   3.3%       0    0.003s
- └─lia --------------------------------------   0.1%   2.4%      28    0.014s
+─tac ----------------------------------------   0.1% 100.0%       1    1.242s
+ ├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  97.6%      26    0.094s
+ │└&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  97.5%      26    0.094s
+ │└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  97.5%      26    0.094s
+ │└t_tauto_intuit ---------------------------   0.1%  97.4%      26    0.094s
+ │ ├─&lt;Corelib.Init.Tauto.simplif&gt; -----------  61.8%  93.7%      26    0.092s
+ │ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; ---------  20.7%  20.7%   28756    0.003s
+ │ │ ├─clear (hyp_list) ---------------------   4.4%   4.4%     650    0.048s
+ │ │ └─elim id ------------------------------   4.0%   4.0%     650    0.003s
+ │ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------   2.6%   3.6%       0    0.005s
+ └─lia --------------------------------------   0.1%   2.1%      28    0.012s
 </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.166s
+</span></dt><dd><span>total time:      1.242s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘
-─lia --   0.1%   2.4%      28    0.014s
+─lia --   0.1%   2.1%      28    0.012s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘

master/refman/.doctrees/addendum/program.doctree

@@ -2639,15 +2639,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.072 secs (0.039u,0.033s) (successful)
+</span></dt><dd><span>Finished transaction in 0.108 secs (0.041u,0.066s) (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.48 secs (0.468u,0.012s) (successful)
+</span></dt><dd><span>Finished transaction in 0.629 secs (0.613u,0.014s) (successful)
 1 goal
 
   H : id (fact 8)</span><span> =</span><span> fact 8
@@ -2675,7 +2675,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
@@ -2710,7 +2710,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.u,0.001s) (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