Deploying to gh-pages from @ 0066a3a 🚀

tutorial_coq_elpi_command.html

@@ -822,7 +822,7 @@ <h1><a class="toc-backref" href="#toc-entry-13">Parsing and Execution</a></h1>
 <span class="si">}}</span>.</span><span class="alectryon-wsp">
 </span></span><span class="alectryon-sentence"><span class="alectryon-input"><span class="kn">Elpi</span> <span class="kn">Typecheck</span>.</span><span class="alectryon-wsp">
 </span></span><span class="alectryon-wsp">
-</span><span class="alectryon-sentence"><input class="alectryon-toggle" id="tutorial-coq-elpi-command-v-chk20" style="display: none" type="checkbox"><label class="alectryon-input" for="tutorial-coq-elpi-command-v-chk20"><span class="kn">Elpi</span> mk_random_module.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message">The module <span class="kr">is</span> «tutorial_coq_elpi_command.Module23»</blockquote></div></div></small></span></pre><p>If the only data to be passed to the interp phase is the list of
+</span><span class="alectryon-sentence"><input class="alectryon-toggle" id="tutorial-coq-elpi-command-v-chk20" style="display: none" type="checkbox"><label class="alectryon-input" for="tutorial-coq-elpi-command-v-chk20"><span class="kn">Elpi</span> mk_random_module.</label><small class="alectryon-output"><div><div class="alectryon-messages"><blockquote class="alectryon-message">The module <span class="kr">is</span> «tutorial_coq_elpi_command.Module71»</blockquote></div></div></small></span></pre><p>If the only data to be passed to the interp phase is the list of
 synterp actions, then a few APIs can come in handy.
 The synterp phase has access to the API <a class="builtin-synterp ghref reference external" href="https://github.com/LPCIC/coq-elpi/blob/0066a3aa0a86375de7601cd67571eff58a28f392/coq-builtin-synterp.elpi#L362">coq.synterp-actions</a>
 that lists the actions performed so far. The interp phase can use

tutorial_elpi_lang.html

@@ -1258,7 +1258,7 @@ <h2><a class="toc-backref" href="#toc-entry-16">Trace browser</a></h2>
 </blockquote><blockquote class="alectryon-message">rid:<span class="mi">1</span> step:<span class="mi">2</span> gid:<span class="mi">16</span> user:subgoal = <span class="mi">18</span> 
 </blockquote><blockquote class="alectryon-message">rid:<span class="mi">1</span> step:<span class="mi">2</span> gid:<span class="mi">18</span> user:newgoal = pi c0 \ of c0 X1 =&gt; of (app c0 c0) X2 
 </blockquote><blockquote class="alectryon-message">rid:<span class="mi">1</span> step:<span class="mi">2</span> gid:<span class="mi">18</span> user:rule:backchain = success 
-</blockquote><blockquote class="alectryon-message">}}} -&gt;  (<span class="mi">0</span>.<span class="mi">001</span>s)</blockquote><blockquote class="alectryon-message">run <span class="mi">3</span> {{{  
+</blockquote><blockquote class="alectryon-message">}}} -&gt;  (<span class="mi">0</span>.<span class="mi">000</span>s)</blockquote><blockquote class="alectryon-message">run <span class="mi">3</span> {{{  
 </blockquote><blockquote class="alectryon-message">rid:<span class="mi">1</span> step:<span class="mi">3</span> gid:<span class="mi">18</span> user:curgoal = pi 
                                    pi c0 \ of c0 X1 =&gt; of (app c0 c0) X2 
 </blockquote><blockquote class="alectryon-message">rid:<span class="mi">1</span> step:<span class="mi">3</span> gid:<span class="mi">18</span> user:rule = pi 
@@ -1303,7 +1303,7 @@ <h2><a class="toc-backref" href="#toc-entry-16">Trace browser</a></h2>
                                           .X5 
 </blockquote><blockquote class="alectryon-message">rid:<span class="mi">1</span> step:<span class="mi">6</span> gid:<span class="mi">0</span> user:assign = X1 := arr X5 X2 
 </blockquote><blockquote class="alectryon-message">rid:<span class="mi">1</span> step:<span class="mi">6</span> gid:<span class="mi">21</span> user:rule:backchain = success 
-</blockquote><blockquote class="alectryon-message">}}} -&gt;  (<span class="mi">0</span>.<span class="mi">001</span>s)</blockquote><blockquote class="alectryon-message">run <span class="mi">7</span> {{{  
+</blockquote><blockquote class="alectryon-message">}}} -&gt;  (<span class="mi">0</span>.<span class="mi">000</span>s)</blockquote><blockquote class="alectryon-message">run <span class="mi">7</span> {{{  
 </blockquote><blockquote class="alectryon-message">rid:<span class="mi">1</span> step:<span class="mi">7</span> gid:<span class="mi">22</span> user:curgoal = of 
                                    of c0 X5 
 </blockquote><blockquote class="alectryon-message">rid:<span class="mi">1</span> step:<span class="mi">7</span> gid:<span class="mi">22</span> user:rule = backchain