Skip to content

Commit

Permalink
Documentation of branch “v9.0” at d093fb20
Browse files Browse the repository at this point in the history
  • Loading branch information
@coqbot
coqbot committed Jan 24, 2025
1 parent 8fe5924 commit b395382
Show file tree
Hide file tree
Showing 52 changed files with 97 additions and 97 deletions.
Binary file modified v9.0/refman-stdlib/.doctrees/environment.pickle
View file
Binary file not shown.
Binary file modified v9.0/refman-stdlib/.doctrees/language/coq-library.doctree
View file
Binary file not shown.
66 changes: 33 additions & 33 deletions v9.0/refman-stdlib/_static/pygments.css
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,70 +6,70 @@ span.linenos.special { color: #000000; background-color: #ffffc0; padding-left:
.highlight .hll { background-color: #ffffcc }
.highlight { background: #eeffcc; }
.highlight .c { color: #408090; font-style: italic } /* Comment */
.highlight .err { border: 1px solid #FF0000 } /* Error */
.highlight .err { border: 1px solid #F00 } /* Error */
.highlight .k { color: #007020; font-weight: bold } /* Keyword */
.highlight .o { color: #666666 } /* Operator */
.highlight .o { color: #666 } /* Operator */
.highlight .ch { color: #408090; font-style: italic } /* Comment.Hashbang */
.highlight .cm { color: #408090; font-style: italic } /* Comment.Multiline */
.highlight .cp { color: #007020 } /* Comment.Preproc */
.highlight .cpf { color: #408090; font-style: italic } /* Comment.PreprocFile */
.highlight .c1 { color: #408090; font-style: italic } /* Comment.Single */
.highlight .cs { color: #408090; background-color: #fff0f0 } /* Comment.Special */
.highlight .cs { color: #408090; background-color: #FFF0F0 } /* Comment.Special */
.highlight .gd { color: #A00000 } /* Generic.Deleted */
.highlight .ge { font-style: italic } /* Generic.Emph */
.highlight .ges { font-weight: bold; font-style: italic } /* Generic.EmphStrong */
.highlight .gr { color: #FF0000 } /* Generic.Error */
.highlight .gr { color: #F00 } /* Generic.Error */
.highlight .gh { color: #000080; font-weight: bold } /* Generic.Heading */
.highlight .gi { color: #00A000 } /* Generic.Inserted */
.highlight .go { color: #333333 } /* Generic.Output */
.highlight .gp { color: #c65d09; font-weight: bold } /* Generic.Prompt */
.highlight .go { color: #333 } /* Generic.Output */
.highlight .gp { color: #C65D09; font-weight: bold } /* Generic.Prompt */
.highlight .gs { font-weight: bold } /* Generic.Strong */
.highlight .gu { color: #800080; font-weight: bold } /* Generic.Subheading */
.highlight .gt { color: #0044DD } /* Generic.Traceback */
.highlight .gt { color: #04D } /* Generic.Traceback */
.highlight .kc { color: #007020; font-weight: bold } /* Keyword.Constant */
.highlight .kd { color: #007020; font-weight: bold } /* Keyword.Declaration */
.highlight .kn { color: #007020; font-weight: bold } /* Keyword.Namespace */
.highlight .kp { color: #007020 } /* Keyword.Pseudo */
.highlight .kr { color: #007020; font-weight: bold } /* Keyword.Reserved */
.highlight .kt { color: #902000 } /* Keyword.Type */
.highlight .m { color: #208050 } /* Literal.Number */
.highlight .s { color: #4070a0 } /* Literal.String */
.highlight .na { color: #4070a0 } /* Name.Attribute */
.highlight .s { color: #4070A0 } /* Literal.String */
.highlight .na { color: #4070A0 } /* Name.Attribute */
.highlight .nb { color: #007020 } /* Name.Builtin */
.highlight .nc { color: #0e84b5; font-weight: bold } /* Name.Class */
.highlight .no { color: #60add5 } /* Name.Constant */
.highlight .nd { color: #555555; font-weight: bold } /* Name.Decorator */
.highlight .ni { color: #d55537; font-weight: bold } /* Name.Entity */
.highlight .nc { color: #0E84B5; font-weight: bold } /* Name.Class */
.highlight .no { color: #60ADD5 } /* Name.Constant */
.highlight .nd { color: #555; font-weight: bold } /* Name.Decorator */
.highlight .ni { color: #D55537; font-weight: bold } /* Name.Entity */
.highlight .ne { color: #007020 } /* Name.Exception */
.highlight .nf { color: #06287e } /* Name.Function */
.highlight .nf { color: #06287E } /* Name.Function */
.highlight .nl { color: #002070; font-weight: bold } /* Name.Label */
.highlight .nn { color: #0e84b5; font-weight: bold } /* Name.Namespace */
.highlight .nn { color: #0E84B5; font-weight: bold } /* Name.Namespace */
.highlight .nt { color: #062873; font-weight: bold } /* Name.Tag */
.highlight .nv { color: #bb60d5 } /* Name.Variable */
.highlight .nv { color: #BB60D5 } /* Name.Variable */
.highlight .ow { color: #007020; font-weight: bold } /* Operator.Word */
.highlight .w { color: #bbbbbb } /* Text.Whitespace */
.highlight .w { color: #BBB } /* Text.Whitespace */
.highlight .mb { color: #208050 } /* Literal.Number.Bin */
.highlight .mf { color: #208050 } /* Literal.Number.Float */
.highlight .mh { color: #208050 } /* Literal.Number.Hex */
.highlight .mi { color: #208050 } /* Literal.Number.Integer */
.highlight .mo { color: #208050 } /* Literal.Number.Oct */
.highlight .sa { color: #4070a0 } /* Literal.String.Affix */
.highlight .sb { color: #4070a0 } /* Literal.String.Backtick */
.highlight .sc { color: #4070a0 } /* Literal.String.Char */
.highlight .dl { color: #4070a0 } /* Literal.String.Delimiter */
.highlight .sd { color: #4070a0; font-style: italic } /* Literal.String.Doc */
.highlight .s2 { color: #4070a0 } /* Literal.String.Double */
.highlight .se { color: #4070a0; font-weight: bold } /* Literal.String.Escape */
.highlight .sh { color: #4070a0 } /* Literal.String.Heredoc */
.highlight .si { color: #70a0d0; font-style: italic } /* Literal.String.Interpol */
.highlight .sx { color: #c65d09 } /* Literal.String.Other */
.highlight .sa { color: #4070A0 } /* Literal.String.Affix */
.highlight .sb { color: #4070A0 } /* Literal.String.Backtick */
.highlight .sc { color: #4070A0 } /* Literal.String.Char */
.highlight .dl { color: #4070A0 } /* Literal.String.Delimiter */
.highlight .sd { color: #4070A0; font-style: italic } /* Literal.String.Doc */
.highlight .s2 { color: #4070A0 } /* Literal.String.Double */
.highlight .se { color: #4070A0; font-weight: bold } /* Literal.String.Escape */
.highlight .sh { color: #4070A0 } /* Literal.String.Heredoc */
.highlight .si { color: #70A0D0; font-style: italic } /* Literal.String.Interpol */
.highlight .sx { color: #C65D09 } /* Literal.String.Other */
.highlight .sr { color: #235388 } /* Literal.String.Regex */
.highlight .s1 { color: #4070a0 } /* Literal.String.Single */
.highlight .s1 { color: #4070A0 } /* Literal.String.Single */
.highlight .ss { color: #517918 } /* Literal.String.Symbol */
.highlight .bp { color: #007020 } /* Name.Builtin.Pseudo */
.highlight .fm { color: #06287e } /* Name.Function.Magic */
.highlight .vc { color: #bb60d5 } /* Name.Variable.Class */
.highlight .vg { color: #bb60d5 } /* Name.Variable.Global */
.highlight .vi { color: #bb60d5 } /* Name.Variable.Instance */
.highlight .vm { color: #bb60d5 } /* Name.Variable.Magic */
.highlight .fm { color: #06287E } /* Name.Function.Magic */
.highlight .vc { color: #BB60D5 } /* Name.Variable.Class */
.highlight .vg { color: #BB60D5 } /* Name.Variable.Global */
.highlight .vi { color: #BB60D5 } /* Name.Variable.Instance */
.highlight .vm { color: #BB60D5 } /* Name.Variable.Magic */
.highlight .il { color: #208050 } /* Literal.Number.Integer.Long */
Binary file modified v9.0/refman/.doctrees/addendum/extraction.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/addendum/generalized-rewriting.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/addendum/implicit-coercions.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/addendum/micromega.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/addendum/miscellaneous-extensions.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/addendum/program.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/addendum/rewrite-rules.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/addendum/ring.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/addendum/sprop.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/addendum/type-classes.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/addendum/universe-polymorphism.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/changes.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/environment.pickle
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/cic.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/coq-library.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/core/assumptions.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/core/basic.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/core/coinductive.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/core/conversion.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/core/inductive.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/core/modules.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/core/primitive.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/core/records.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/core/sections.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/core/variants.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/extensions/arguments-command.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/extensions/canonical.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/extensions/evars.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/extensions/implicit-arguments.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/language/extensions/match.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/practical-tools/coq-commands.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/practical-tools/coqide.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/proof-engine/ltac.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/proof-engine/ltac2.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/proof-engine/tactics.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/proof-engine/vernacular-commands.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/proofs/automatic-tactics/auto.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/proofs/automatic-tactics/logic.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/proofs/writing-proofs/equality.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/user-extensions/syntax-extensions.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/using/libraries/funind.doctree
View file
Binary file not shown.
Binary file modified v9.0/refman/.doctrees/using/libraries/writing.doctree
View file
Binary file not shown.
66 changes: 33 additions & 33 deletions v9.0/refman/_static/pygments.css
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,70 +6,70 @@ span.linenos.special { color: #000000; background-color: #ffffc0; padding-left:
.highlight .hll { background-color: #ffffcc }
.highlight { background: #eeffcc; }
.highlight .c { color: #408090; font-style: italic } /* Comment */
.highlight .err { border: 1px solid #FF0000 } /* Error */
.highlight .err { border: 1px solid #F00 } /* Error */
.highlight .k { color: #007020; font-weight: bold } /* Keyword */
.highlight .o { color: #666666 } /* Operator */
.highlight .o { color: #666 } /* Operator */
.highlight .ch { color: #408090; font-style: italic } /* Comment.Hashbang */
.highlight .cm { color: #408090; font-style: italic } /* Comment.Multiline */
.highlight .cp { color: #007020 } /* Comment.Preproc */
.highlight .cpf { color: #408090; font-style: italic } /* Comment.PreprocFile */
.highlight .c1 { color: #408090; font-style: italic } /* Comment.Single */
.highlight .cs { color: #408090; background-color: #fff0f0 } /* Comment.Special */
.highlight .cs { color: #408090; background-color: #FFF0F0 } /* Comment.Special */
.highlight .gd { color: #A00000 } /* Generic.Deleted */
.highlight .ge { font-style: italic } /* Generic.Emph */
.highlight .ges { font-weight: bold; font-style: italic } /* Generic.EmphStrong */
.highlight .gr { color: #FF0000 } /* Generic.Error */
.highlight .gr { color: #F00 } /* Generic.Error */
.highlight .gh { color: #000080; font-weight: bold } /* Generic.Heading */
.highlight .gi { color: #00A000 } /* Generic.Inserted */
.highlight .go { color: #333333 } /* Generic.Output */
.highlight .gp { color: #c65d09; font-weight: bold } /* Generic.Prompt */
.highlight .go { color: #333 } /* Generic.Output */
.highlight .gp { color: #C65D09; font-weight: bold } /* Generic.Prompt */
.highlight .gs { font-weight: bold } /* Generic.Strong */
.highlight .gu { color: #800080; font-weight: bold } /* Generic.Subheading */
.highlight .gt { color: #0044DD } /* Generic.Traceback */
.highlight .gt { color: #04D } /* Generic.Traceback */
.highlight .kc { color: #007020; font-weight: bold } /* Keyword.Constant */
.highlight .kd { color: #007020; font-weight: bold } /* Keyword.Declaration */
.highlight .kn { color: #007020; font-weight: bold } /* Keyword.Namespace */
.highlight .kp { color: #007020 } /* Keyword.Pseudo */
.highlight .kr { color: #007020; font-weight: bold } /* Keyword.Reserved */
.highlight .kt { color: #902000 } /* Keyword.Type */
.highlight .m { color: #208050 } /* Literal.Number */
.highlight .s { color: #4070a0 } /* Literal.String */
.highlight .na { color: #4070a0 } /* Name.Attribute */
.highlight .s { color: #4070A0 } /* Literal.String */
.highlight .na { color: #4070A0 } /* Name.Attribute */
.highlight .nb { color: #007020 } /* Name.Builtin */
.highlight .nc { color: #0e84b5; font-weight: bold } /* Name.Class */
.highlight .no { color: #60add5 } /* Name.Constant */
.highlight .nd { color: #555555; font-weight: bold } /* Name.Decorator */
.highlight .ni { color: #d55537; font-weight: bold } /* Name.Entity */
.highlight .nc { color: #0E84B5; font-weight: bold } /* Name.Class */
.highlight .no { color: #60ADD5 } /* Name.Constant */
.highlight .nd { color: #555; font-weight: bold } /* Name.Decorator */
.highlight .ni { color: #D55537; font-weight: bold } /* Name.Entity */
.highlight .ne { color: #007020 } /* Name.Exception */
.highlight .nf { color: #06287e } /* Name.Function */
.highlight .nf { color: #06287E } /* Name.Function */
.highlight .nl { color: #002070; font-weight: bold } /* Name.Label */
.highlight .nn { color: #0e84b5; font-weight: bold } /* Name.Namespace */
.highlight .nn { color: #0E84B5; font-weight: bold } /* Name.Namespace */
.highlight .nt { color: #062873; font-weight: bold } /* Name.Tag */
.highlight .nv { color: #bb60d5 } /* Name.Variable */
.highlight .nv { color: #BB60D5 } /* Name.Variable */
.highlight .ow { color: #007020; font-weight: bold } /* Operator.Word */
.highlight .w { color: #bbbbbb } /* Text.Whitespace */
.highlight .w { color: #BBB } /* Text.Whitespace */
.highlight .mb { color: #208050 } /* Literal.Number.Bin */
.highlight .mf { color: #208050 } /* Literal.Number.Float */
.highlight .mh { color: #208050 } /* Literal.Number.Hex */
.highlight .mi { color: #208050 } /* Literal.Number.Integer */
.highlight .mo { color: #208050 } /* Literal.Number.Oct */
.highlight .sa { color: #4070a0 } /* Literal.String.Affix */
.highlight .sb { color: #4070a0 } /* Literal.String.Backtick */
.highlight .sc { color: #4070a0 } /* Literal.String.Char */
.highlight .dl { color: #4070a0 } /* Literal.String.Delimiter */
.highlight .sd { color: #4070a0; font-style: italic } /* Literal.String.Doc */
.highlight .s2 { color: #4070a0 } /* Literal.String.Double */
.highlight .se { color: #4070a0; font-weight: bold } /* Literal.String.Escape */
.highlight .sh { color: #4070a0 } /* Literal.String.Heredoc */
.highlight .si { color: #70a0d0; font-style: italic } /* Literal.String.Interpol */
.highlight .sx { color: #c65d09 } /* Literal.String.Other */
.highlight .sa { color: #4070A0 } /* Literal.String.Affix */
.highlight .sb { color: #4070A0 } /* Literal.String.Backtick */
.highlight .sc { color: #4070A0 } /* Literal.String.Char */
.highlight .dl { color: #4070A0 } /* Literal.String.Delimiter */
.highlight .sd { color: #4070A0; font-style: italic } /* Literal.String.Doc */
.highlight .s2 { color: #4070A0 } /* Literal.String.Double */
.highlight .se { color: #4070A0; font-weight: bold } /* Literal.String.Escape */
.highlight .sh { color: #4070A0 } /* Literal.String.Heredoc */
.highlight .si { color: #70A0D0; font-style: italic } /* Literal.String.Interpol */
.highlight .sx { color: #C65D09 } /* Literal.String.Other */
.highlight .sr { color: #235388 } /* Literal.String.Regex */
.highlight .s1 { color: #4070a0 } /* Literal.String.Single */
.highlight .s1 { color: #4070A0 } /* Literal.String.Single */
.highlight .ss { color: #517918 } /* Literal.String.Symbol */
.highlight .bp { color: #007020 } /* Name.Builtin.Pseudo */
.highlight .fm { color: #06287e } /* Name.Function.Magic */
.highlight .vc { color: #bb60d5 } /* Name.Variable.Class */
.highlight .vg { color: #bb60d5 } /* Name.Variable.Global */
.highlight .vi { color: #bb60d5 } /* Name.Variable.Instance */
.highlight .vm { color: #bb60d5 } /* Name.Variable.Magic */
.highlight .fm { color: #06287E } /* Name.Function.Magic */
.highlight .vc { color: #BB60D5 } /* Name.Variable.Class */
.highlight .vg { color: #BB60D5 } /* Name.Variable.Global */
.highlight .vi { color: #BB60D5 } /* Name.Variable.Instance */
.highlight .vm { color: #BB60D5 } /* Name.Variable.Magic */
.highlight .il { color: #208050 } /* Literal.Number.Integer.Long */
50 changes: 25 additions & 25 deletions v9.0/refman/proof-engine/ltac.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4292,42 +4292,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.366s
</span></dt><dd><span>total time: 1.442s

tactic local total calls max
───────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─tac -------------------------------------- 0.1% 100.0% 1 1.366s
─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; -- 0.0% 92.7% 26 0.135s
─&lt;Corelib.Init.Tauto.tauto_gen&gt; ----------- 0.0% 92.6% 26 0.135s
─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt; 0.0% 92.6% 26 0.135s
─t_tauto_intuit --------------------------- 0.1% 92.5% 26 0.135s
─&lt;Corelib.Init.Tauto.simplif&gt; ------------- 60.2% 89.1% 26 0.132s
─&lt;Corelib.Init.Tauto.is_conj&gt; ------------- 21.7% 21.7% 28756 0.033s
─lia -------------------------------------- 0.1% 7.0% 28 0.064s
─Zify.zify -------------------------------- 4.9% 5.5% 54 0.063s
─elim id ---------------------------------- 3.6% 3.6% 650 0.001s
─&lt;Corelib.Init.Tauto.axioms&gt; -------------- 2.3% 3.4% 0 0.003s
─tac -------------------------------------- 0.1% 100.0% 1 1.442s
─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; -- 0.0% 93.0% 26 0.132s
─&lt;Corelib.Init.Tauto.tauto_gen&gt; ----------- 0.0% 92.9% 26 0.132s
─&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt; 0.1% 92.9% 26 0.132s
─t_tauto_intuit --------------------------- 0.1% 92.8% 26 0.132s
─&lt;Corelib.Init.Tauto.simplif&gt; ------------- 61.0% 89.4% 26 0.130s
─&lt;Corelib.Init.Tauto.is_conj&gt; ------------- 21.3% 21.3% 28756 0.028s
─lia -------------------------------------- 0.1% 6.7% 28 0.065s
─Zify.zify -------------------------------- 4.8% 5.3% 54 0.065s
─elim id ---------------------------------- 3.7% 3.7% 650 0.001s
─&lt;Corelib.Init.Tauto.axioms&gt; -------------- 2.4% 3.3% 0 0.004s

tactic local total calls max
─────────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─tac ---------------------------------------- 0.1% 100.0% 1 1.366s
├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; -- 0.0% 92.7% 26 0.135s
│└&lt;Corelib.Init.Tauto.tauto_gen&gt; ----------- 0.0% 92.6% 26 0.135s
│└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt; 0.0% 92.6% 26 0.135s
│└t_tauto_intuit --------------------------- 0.1% 92.5% 26 0.135s
│ ├─&lt;Corelib.Init.Tauto.simplif&gt; ----------- 60.2% 89.1% 26 0.132s
│ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; --------- 21.7% 21.7% 28756 0.033s
│ │ └─elim id ------------------------------ 3.6% 3.6% 650 0.001s
│ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------ 2.3% 3.4% 0 0.003s
└─lia -------------------------------------- 0.1% 7.0% 28 0.064s
└Zify.zify -------------------------------- 4.9% 5.5% 54 0.063s
─tac ---------------------------------------- 0.1% 100.0% 1 1.442s
├─&lt;Corelib.Init.Tauto.with_uniform_flags&gt; -- 0.0% 93.0% 26 0.132s
│└&lt;Corelib.Init.Tauto.tauto_gen&gt; ----------- 0.0% 92.9% 26 0.132s
│└&lt;Corelib.Init.Tauto.tauto_intuitionistic&gt; 0.1% 92.9% 26 0.132s
│└t_tauto_intuit --------------------------- 0.1% 92.8% 26 0.132s
│ ├─&lt;Corelib.Init.Tauto.simplif&gt; ----------- 61.0% 89.4% 26 0.130s
│ │ ├─&lt;Corelib.Init.Tauto.is_conj&gt; --------- 21.3% 21.3% 28756 0.028s
│ │ └─elim id ------------------------------ 3.7% 3.7% 650 0.001s
│ └─&lt;Corelib.Init.Tauto.axioms&gt; ------------ 2.4% 3.3% 0 0.004s
└─lia -------------------------------------- 0.1% 6.7% 28 0.065s
└Zify.zify -------------------------------- 4.8% 5.3% 54 0.065s
</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.366s
</span></dt><dd><span>total time: 1.442s

tactic local total calls max
───────┴──────┴──────┴───────┴─────────┘
─lia -- 0.1% 7.0% 28 0.064s
─lia -- 0.1% 6.7% 28 0.065s

tactic local total calls max
───────┴──────┴──────┴───────┴─────────┘
Expand Down
Loading

0 comments on commit b395382

Please sign in to comment.