Skip to content

Commit

Permalink
Deploying to gh-pages from @ 006047a 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed Jun 25, 2024
1 parent f1ce42b commit c597706
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 @@ -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.Module12»</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.Module24»</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/006047acd2c74a2b7ec395f5282ac13f9f8f1d0e/builtin-doc/coq-builtin-synterp.elpi#L365">coq.synterp-actions</a>
that lists the actions performed so far. The interp phase can use
Expand Down

0 comments on commit c597706

Please sign in to comment.