Documentation of branch “master” at 9edc9980

coq · Dec 20, 2024 · 2a940f7 · 2a940f7
1 parent ebb8e58
commit 2a940f7
Show file tree

Hide file tree

Showing 28 changed files with 31 additions and 33 deletions.
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/program.doctree b/master/refman/.doctrees/addendum/program.doctree
diff --git a/master/refman/.doctrees/addendum/rewrite-rules.doctree b/master/refman/.doctrees/addendum/rewrite-rules.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/environment.pickle b/master/refman/.doctrees/environment.pickle
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/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/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/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/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
@@ -4285,42 +4285,40 @@ <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.055s
+</span></dt><dd><span>total time:      2.067s
 
  tactic                                      local  total   calls       max
 ───────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac --------------------------------------   0.1% 100.0%       1    1.055s
-─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  97.7%      26    0.072s
-─&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  97.7%      26    0.071s
-─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  97.6%      26    0.071s
-─t_tauto_intuit ---------------------------   0.1%  97.5%      26    0.071s
-─&lt;Corelib.Init.Tauto.simplif&gt; -------------  61.0%  93.8%      26    0.070s
-─&lt;Corelib.Init.Tauto.is_conj&gt; -------------  22.3%  22.3%   28756    0.003s
-─clear (hyp_list) -------------------------   3.8%   3.8%     650    0.035s
-─elim id ----------------------------------   3.7%   3.7%     650    0.002s
-─&lt;Corelib.Init.Tauto.axioms&gt; --------------   2.6%   3.6%       0    0.005s
-─lia --------------------------------------   0.1%   2.0%      28    0.009s
+─tac --------------------------------------   0.1% 100.0%       1    2.067s
+─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  98.0%      26    0.152s
+─&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  97.9%      26    0.152s
+─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.0%  97.9%      26    0.152s
+─t_tauto_intuit ---------------------------   0.1%  97.8%      26    0.152s
+─&lt;Corelib.Init.Tauto.simplif&gt; -------------  62.4%  94.3%      26    0.149s
+─&lt;Corelib.Init.Tauto.is_conj&gt; -------------  21.6%  21.6%   28756    0.040s
+─elim id ----------------------------------   4.1%   4.1%     650    0.003s
+─&lt;Corelib.Init.Tauto.axioms&gt; --------------   2.5%   3.4%       0    0.006s
+─clear (hyp_list) -------------------------   3.2%   3.2%     650    0.055s
 
- tactic                                        local  total   calls       max
-─────────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac ----------------------------------------   0.1% 100.0%       1    1.055s
- ├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  97.7%      26    0.072s
- │└&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  97.7%      26    0.071s
- │└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.1%  97.6%      26    0.071s
- │└t_tauto_intuit ---------------------------   0.1%  97.5%      26    0.071s
- │ ├─&lt;Corelib.Init.Tauto.simplif&gt; -----------  61.0%  93.8%      26    0.070s
- │ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; ---------  22.3%  22.3%   28756    0.003s
- │ │ ├─clear (hyp_list) ---------------------   3.8%   3.8%     650    0.035s
- │ │ └─elim id ------------------------------   3.7%   3.7%     650    0.002s
- │ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------   2.6%   3.6%       0    0.005s
- └─lia --------------------------------------   0.1%   2.0%      28    0.009s
+ tactic                                      local  total   calls       max
+───────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─tac --------------------------------------   0.1% 100.0%       1    2.067s
+└&lt;Corelib.Init.Tauto.with_uniform_flags&gt; --   0.0%  98.0%      26    0.152s
+└&lt;Corelib.Init.Tauto.tauto_gen&gt; -----------   0.0%  97.9%      26    0.152s
+└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt;    0.0%  97.9%      26    0.152s
+└t_tauto_intuit ---------------------------   0.1%  97.8%      26    0.152s
+ ├─&lt;Corelib.Init.Tauto.simplif&gt; -----------  62.4%  94.3%      26    0.149s
+ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; ---------  21.6%  21.6%   28756    0.040s
+ │ ├─elim id ------------------------------   4.1%   4.1%     650    0.003s
+ │ └─clear (hyp_list) ---------------------   3.2%   3.2%     650    0.055s
+ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------   2.5%   3.4%       0    0.006s
 </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.055s
+</span></dt><dd><span>total time:      2.067s
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘
-─lia --   0.1%   2.0%      28    0.009s
+
 
  tactic  local  total   calls       max
 ───────┴──────┴──────┴───────┴─────────┘

diff --git a/master/refman/proofs/writing-proofs/equality.html b/master/refman/proofs/writing-proofs/equality.html
@@ -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.044 secs (0.034u,0.01s) (successful)
+</span></dt><dd><span>Finished transaction in 0.093 secs (0.064u,0.029s) (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.309 secs (0.301u,0.007s) (successful)
+</span></dt><dd><span>Finished transaction in 0.796 secs (0.793u,0.003s) (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. secs (0.u,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
@@ -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.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
@@ -2721,7 +2721,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>

diff --git a/master/refman/searchindex.js b/master/refman/searchindex.js