Documentation of branch “master” at 2c068b8e

master/refman/_sources/addendum/extraction.rst.txt

@@ -12,12 +12,12 @@ functional languages available as output are currently OCaml, Haskell
 and Scheme. In the following, "ML" will be used (abusively) to refer
 to any of the three.
 
-Before using any of the commands or options described in this chapter,
-the extraction framework should first be loaded explicitly
-via ``Require Extraction``, or via the more robust
-``From Coq Require Extraction``.
-Note that in earlier versions of Coq, these commands and options were
-directly available without any preliminary ``Require``.
+.. versionchanged:: 8.11
+
+   Before using any of the commands or options described in this chapter,
+   the extraction framework should first be loaded explicitly
+   via ``Require Extraction``, or via the more robust
+   ``From Coq Require Extraction``.
 
 .. coqtop:: in
 
@@ -50,7 +50,10 @@ Generating ML Code
    requirements of the target language, keeping original
    names as much as possible.
 
-The following commands also generate file(s).
+The following commands also generate file(s). The generated file(s) are
+produced in the current working directory. It is possible to inspect what
+is the current directory with the command :cmd:`Pwd` and to change it with
+the command :cmd:`Cd`.
 
 .. cmd:: Extraction Library @ident
 
@@ -93,6 +96,17 @@ in the Coq sources.
 .. cmd:: Show Extraction
    :undocumented:
 
+.. cmd:: Pwd
+
+   This command displays the current working directory (where the extracted
+   files are produced).
+
+.. cmd:: Cd {? @string }
+
+   If :n:`@string` is specified, changes the current directory according to
+   :token:`string` which can be any valid path.  Otherwise, it displays the
+   current directory as :cmd:`Pwd` does.
+
 Extraction Options
 -------------------
 

master/refman/_sources/proof-engine/vernacular-commands.rst.txt

@@ -717,15 +717,6 @@ Load paths
    removed. Load paths can be managed using Coq command line options or
    enviroment variables (see :ref:`logical-paths-load-path`).
 
-.. cmd:: Pwd
-
-   This command displays the current working directory.
-
-.. cmd:: Cd {? @string }
-
-   If :n:`@string` is specified, changes the current directory according to :token:`string` which
-   can be any valid path.  Otherwise, it displays the current directory.
-
 .. cmd:: Print LoadPath {? @dirpath }
 
    Displays the current Coq :term:`load path`.  If :n:`@dirpath` is specified,

master/refman/addendum/extraction.html

@@ -1241,12 +1241,12 @@
 functional languages available as output are currently OCaml, Haskell
 and Scheme. In the following, "ML" will be used (abusively) to refer
 to any of the three.</p>
-<p>Before using any of the commands or options described in this chapter,
+<div class="versionchanged">
+<p><span class="versionmodified changed">Changed in version 8.11: </span>Before using any of the commands or options described in this chapter,
 the extraction framework should first be loaded explicitly
 via <code class="docutils literal notranslate"><span class="pre">Require</span> <span class="pre">Extraction</span></code>, or via the more robust
-<code class="docutils literal notranslate"><span class="pre">From</span> <span class="pre">Coq</span> <span class="pre">Require</span> <span class="pre">Extraction</span></code>.
-Note that in earlier versions of Coq, these commands and options were
-directly available without any preliminary <code class="docutils literal notranslate"><span class="pre">Require</span></code>.</p>
+<code class="docutils literal notranslate"><span class="pre">From</span> <span class="pre">Coq</span> <span class="pre">Require</span> <span class="pre">Extraction</span></code>.</p>
+</div>
 <div class="coqtop literal-block docutils container">
 <span></span><dl>
 <dt><span></span><span class="coqdoc-keyword">Require</span><span> </span><span class="coqdoc-keyword">Extraction</span><span>.</span><span>
@@ -1283,7 +1283,10 @@ <h2>Generating ML Code<a class="headerlink" href="#generating-ml-code" title="Pe
 names as much as possible.</p>
 </dd></dl>
 
-<p>The following commands also generate file(s).</p>
+<p>The following commands also generate file(s). The generated file(s) are
+produced in the current working directory. It is possible to inspect what
+is the current directory with the command <a class="reference internal" href="#coq:cmd.Pwd" title="Pwd"><code class="xref coq coq-cmd docutils literal notranslate"><span class="pre">Pwd</span></code></a> and to change it with
+the command <a class="reference internal" href="#coq:cmd.Cd" title="Cd"><code class="xref coq coq-cmd docutils literal notranslate"><span class="pre">Cd</span></code></a>.</p>
 <dl class="coq cmd">
 <dt class="sig sig-object coq" id="coq:cmd.Extraction-Library">
 <em class="property"><span class="sigannot"><span class="pre">Command</span></span></em> <span class="sig-name descname"><span class="notation"><span><span><span class="pre">Extraction</span></span></span> <span><span><span class="pre">Library</span></span></span> <a class="reference internal" href="../language/core/basic.html#grammar-token-ident"><span class="hole"><span class="pre">ident</span></span></a></span></span><a class="headerlink" href="#coq:cmd.Extraction-Library" title="Permalink to this definition">¶</a></dt>
@@ -1334,6 +1337,21 @@ <h2>Generating ML Code<a class="headerlink" href="#generating-ml-code" title="Pe
 <em class="property"><span class="sigannot"><span class="pre">Command</span></span></em> <span class="sig-name descname"><span class="notation"><span><span><span class="pre">Show</span></span></span> <span><span><span class="pre">Extraction</span></span></span></span></span><a class="headerlink" href="#coq:cmd.Show-Extraction" title="Permalink to this definition">¶</a></dt>
 <dd></dd></dl>
 
+<dl class="coq cmd">
+<dt class="sig sig-object coq" id="coq:cmd.Pwd">
+<em class="property"><span class="sigannot"><span class="pre">Command</span></span></em> <span class="sig-name descname"><span class="notation"><span><span><span class="pre">Pwd</span></span></span></span></span><a class="headerlink" href="#coq:cmd.Pwd" title="Permalink to this definition">¶</a></dt>
+<dd><p>This command displays the current working directory (where the extracted
+files are produced).</p>
+</dd></dl>
+
+<dl class="coq cmd">
+<dt class="sig sig-object coq" id="coq:cmd.Cd">
+<em class="property"><span class="sigannot"><span class="pre">Command</span></span></em> <span class="sig-name descname"><span class="notation"><span><span><span class="pre">Cd</span></span></span> <span class="repeat-wrapper"><span class="repeat"><a class="reference internal" href="../language/core/basic.html#grammar-token-string"><span class="hole"><span class="pre">string</span></span></a></span><span class="notation-sup"><span class="pre">?</span></span></span></span></span><a class="headerlink" href="#coq:cmd.Cd" title="Permalink to this definition">¶</a></dt>
+<dd><p>If <code class="docutils literal notranslate"><span class="notation"><a class="reference internal" href="../language/core/basic.html#grammar-token-string"><span class="hole"><span class="pre">string</span></span></a></span></code> is specified, changes the current directory according to
+<a class="reference internal" href="../language/core/basic.html#grammar-token-string"><code class="xref std std-token docutils literal notranslate"><span class="pre">string</span></code></a> which can be any valid path.  Otherwise, it displays the
+current directory as <a class="reference internal" href="#coq:cmd.Pwd" title="Pwd"><code class="xref coq coq-cmd docutils literal notranslate"><span class="pre">Pwd</span></code></a> does.</p>
+</dd></dl>
+
 </section>
 <section id="extraction-options">
 <h2>Extraction Options<a class="headerlink" href="#extraction-options" title="Permalink to this headline">¶</a></h2>

master/refman/coq-cmdindex.html

@@ -1300,7 +1300,7 @@ <h1>Command Index</h1>
      <tr>
        <td></td>
        <td>
-       <a href="proof-engine/vernacular-commands.html#coq:cmd.Cd"><code class="xref">Cd</code></a></td><td>
+       <a href="addendum/extraction.html#coq:cmd.Cd"><code class="xref">Cd</code></a></td><td>
        <em></em></td></tr>
      <tr>
        <td></td>
@@ -2333,7 +2333,7 @@ <h1>Command Index</h1>
      <tr>
        <td></td>
        <td>
-       <a href="proof-engine/vernacular-commands.html#coq:cmd.Pwd"><code class="xref">Pwd</code></a></td><td>
+       <a href="addendum/extraction.html#coq:cmd.Pwd"><code class="xref">Pwd</code></a></td><td>
        <em></em></td></tr>
      <tr class="pcap"><td></td><td>&#160;</td><td></td></tr>
      <tr class="cap" id="cap-q"><td></td><td>

master/refman/genindex.html

@@ -1610,7 +1610,7 @@ <h2 id="C">C</h2>
 </li>
       <li><a href="proofs/writing-proofs/equality.html#coq:tacn.cbv">cbv (tactic)</a>
 </li>
-      <li><a href="proof-engine/vernacular-commands.html#coq:cmd.Cd">Cd (command)</a>
+      <li><a href="addendum/extraction.html#coq:cmd.Cd">Cd (command)</a>
 </li>
       <li><a href="proofs/writing-proofs/equality.html#coq:tacn.change">change (tactic)</a>
 </li>
@@ -3171,7 +3171,7 @@ <h2 id="P">P</h2>
 </li>
       <li><a href="proof-engine/vernacular-commands.html#coq:exn.public-name-according-to-findlib,-for-example">public name according to findlib, for example (error)</a>
 </li>
-      <li><a href="proof-engine/vernacular-commands.html#coq:cmd.Pwd">Pwd (command)</a>
+      <li><a href="addendum/extraction.html#coq:cmd.Pwd">Pwd (command)</a>
 </li>
   </ul></td>
 </tr></table>

master/refman/practical-tools/utilities.html

@@ -1418,7 +1418,7 @@ <h3>Setup for working on your own projects<a class="headerlink" href="#setup-for
 permits loading files from the
 associated directory with just the basename of the script file,
 e.g. specify <code class="docutils literal notranslate"><span class="pre">Foo</span></code> to load <code class="docutils literal notranslate"><span class="pre">Foo.vo</span></code>.  This entry corresponds to the
-current directory when Coq was started.  Note that the <a class="reference internal" href="../proof-engine/vernacular-commands.html#coq:cmd.Cd" title="Cd"><code class="xref coq coq-cmd docutils literal notranslate"><span class="pre">Cd</span></code></a> command
+current directory when Coq was started.  Note that the <a class="reference internal" href="../addendum/extraction.html#coq:cmd.Cd" title="Cd"><code class="xref coq coq-cmd docutils literal notranslate"><span class="pre">Cd</span></code></a> command
 doesn't change the associated directory--you would need to restart CoqIDE.</p>
 <p>With some exceptions noted below, the <a class="reference internal" href="#term-load-path"><span class="xref std std-term">load path</span></a> is generated from files loaded
 from the following directories and their subdirectories in the order shown.  The

master/refman/proof-engine/ltac.html

@@ -3314,7 +3314,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. secs (0.u,0.s)
+Tactic evaluation ran for 0.001 secs (0.001u,0.s)
 1 goal
 
   n := 100 : nat
@@ -4227,35 +4227,35 @@ <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.598s
+</span></dt><dd><span>total time:      2.737s
 
  tactic                                   local  total   calls       max 
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac -----------------------------------   3.6% 100.0%       1    2.598s
-─&lt;Coq.Init.Tauto.with_uniform_flags&gt; ---   0.0%  94.6%      26    0.231s
-─&lt;Coq.Init.Tauto.tauto_gen&gt; ------------   0.0%  94.5%      26    0.231s
-─&lt;Coq.Init.Tauto.tauto_intuitionistic&gt; -   0.0%  94.5%      26    0.231s
-─t_tauto_intuit ------------------------   0.1%  94.4%      26    0.231s
-─&lt;Coq.Init.Tauto.simplif&gt; --------------  67.1%  91.5%      26    0.228s
-─&lt;Coq.Init.Tauto.is_conj&gt; --------------  17.1%  17.1%   28756    0.000s
-─elim id -------------------------------   4.1%   4.1%     650    0.002s
-─&lt;Coq.Init.Tauto.axioms&gt; ---------------   2.0%   2.9%       0    0.003s
+─tac -----------------------------------   4.3% 100.0%       1    2.737s
+─&lt;Coq.Init.Tauto.with_uniform_flags&gt; ---   0.0%  93.8%      26    0.219s
+─&lt;Coq.Init.Tauto.tauto_gen&gt; ------------   0.0%  93.7%      26    0.219s
+─&lt;Coq.Init.Tauto.tauto_intuitionistic&gt; -   0.0%  93.7%      26    0.219s
+─t_tauto_intuit ------------------------   0.1%  93.6%      26    0.219s
+─&lt;Coq.Init.Tauto.simplif&gt; --------------  67.0%  90.7%      26    0.216s
+─&lt;Coq.Init.Tauto.is_conj&gt; --------------  16.5%  16.5%   28756    0.000s
+─elim id -------------------------------   4.1%   4.1%     650    0.003s
+─&lt;Coq.Init.Tauto.axioms&gt; ---------------   2.0%   2.8%       0    0.004s
 
  tactic                                   local  total   calls       max 
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
-─tac -----------------------------------   3.6% 100.0%       1    2.598s
-└&lt;Coq.Init.Tauto.with_uniform_flags&gt; ---   0.0%  94.6%      26    0.231s
-└&lt;Coq.Init.Tauto.tauto_gen&gt; ------------   0.0%  94.5%      26    0.231s
-└&lt;Coq.Init.Tauto.tauto_intuitionistic&gt; -   0.0%  94.5%      26    0.231s
-└t_tauto_intuit ------------------------   0.1%  94.4%      26    0.231s
- ├─&lt;Coq.Init.Tauto.simplif&gt; ------------  67.1%  91.5%      26    0.228s
- │ ├─&lt;Coq.Init.Tauto.is_conj&gt; ----------  17.1%  17.1%   28756    0.000s
- │ └─elim id ---------------------------   4.1%   4.1%     650    0.002s
- └─&lt;Coq.Init.Tauto.axioms&gt; -------------   2.0%   2.9%       0    0.003s
+─tac -----------------------------------   4.3% 100.0%       1    2.737s
+└&lt;Coq.Init.Tauto.with_uniform_flags&gt; ---   0.0%  93.8%      26    0.219s
+└&lt;Coq.Init.Tauto.tauto_gen&gt; ------------   0.0%  93.7%      26    0.219s
+└&lt;Coq.Init.Tauto.tauto_intuitionistic&gt; -   0.0%  93.7%      26    0.219s
+└t_tauto_intuit ------------------------   0.1%  93.6%      26    0.219s
+ ├─&lt;Coq.Init.Tauto.simplif&gt; ------------  67.0%  90.7%      26    0.216s
+ │ ├─&lt;Coq.Init.Tauto.is_conj&gt; ----------  16.5%  16.5%   28756    0.000s
+ │ └─elim id ---------------------------   4.1%   4.1%     650    0.003s
+ └─&lt;Coq.Init.Tauto.axioms&gt; -------------   2.0%   2.8%       0    0.004s
 
 </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.598s
+</span></dt><dd><span>total time:      2.737s
 
  tactic                                   local  total   calls       max 
 ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘

master/refman/proof-engine/vernacular-commands.html

@@ -2139,19 +2139,6 @@ <h2>Load paths<a class="headerlink" href="#load-paths" title="Permalink to this
 removed. Load paths can be managed using Coq command line options or
 enviroment variables (see <a class="reference internal" href="../practical-tools/utilities.html#logical-paths-load-path"><span class="std std-ref">Logical paths and the load path</span></a>).</p>
 </div>
-<dl class="coq cmd">
-<dt class="sig sig-object coq" id="coq:cmd.Pwd">
-<em class="property"><span class="sigannot"><span class="pre">Command</span></span></em> <span class="sig-name descname"><span class="notation"><span><span><span class="pre">Pwd</span></span></span></span></span><a class="headerlink" href="#coq:cmd.Pwd" title="Permalink to this definition">¶</a></dt>
-<dd><p>This command displays the current working directory.</p>
-</dd></dl>
-
-<dl class="coq cmd">
-<dt class="sig sig-object coq" id="coq:cmd.Cd">
-<em class="property"><span class="sigannot"><span class="pre">Command</span></span></em> <span class="sig-name descname"><span class="notation"><span><span><span class="pre">Cd</span></span></span> <span class="repeat-wrapper"><span class="repeat"><a class="reference internal" href="../language/core/basic.html#grammar-token-string"><span class="hole"><span class="pre">string</span></span></a></span><span class="notation-sup"><span class="pre">?</span></span></span></span></span><a class="headerlink" href="#coq:cmd.Cd" title="Permalink to this definition">¶</a></dt>
-<dd><p>If <code class="docutils literal notranslate"><span class="notation"><a class="reference internal" href="../language/core/basic.html#grammar-token-string"><span class="hole"><span class="pre">string</span></span></a></span></code> is specified, changes the current directory according to <a class="reference internal" href="../language/core/basic.html#grammar-token-string"><code class="xref std std-token docutils literal notranslate"><span class="pre">string</span></code></a> which
-can be any valid path.  Otherwise, it displays the current directory.</p>
-</dd></dl>
-
 <dl class="coq cmd">
 <dt class="sig sig-object coq" id="coq:cmd.Print-LoadPath">
 <em class="property"><span class="sigannot"><span class="pre">Command</span></span></em> <span class="sig-name descname"><span class="notation"><span><span><span class="pre">Print</span></span></span> <span><span><span class="pre">LoadPath</span></span></span> <span class="repeat-wrapper"><span class="repeat"><a class="reference internal" href="#grammar-token-dirpath"><span class="hole"><span class="pre">dirpath</span></span></a></span><span class="notation-sup"><span class="pre">?</span></span></span></span></span><a class="headerlink" href="#coq:cmd.Print-LoadPath" title="Permalink to this definition">¶</a></dt>