Skip to content

Commit

Permalink
Deploying to gh-pages from @ ed38e16 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed Dec 6, 2024
1 parent b22e180 commit efb006e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion tutorial_coq_elpi_command.html
Original file line number Diff line number Diff line change
Expand Up @@ -823,7 +823,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-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.Module38»</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.Module81»</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="reference external builtin-synterp ghref" href="https://github.com/LPCIC/coq-elpi/blob/ed38e16f6620dca4340d95b89c62346c7df03552/builtin-doc/coq-builtin-synterp.elpi#L380">coq.synterp-actions</a>
that lists the actions performed so far. The interp phase can use
Expand Down

0 comments on commit efb006e

Please sign in to comment.