diff --git a/tutorial_coq_elpi_command.html b/tutorial_coq_elpi_command.html index 183156b63..fe5f1e4cd 100644 --- a/tutorial_coq_elpi_command.html +++ b/tutorial_coq_elpi_command.html @@ -822,7 +822,7 @@

Parsing and Execution

}}. Elpi Typecheck. -
The module is «tutorial_coq_elpi_command.Module7»

If the only data to be passed to the interp phase is the list of +

The module is «tutorial_coq_elpi_command.Module58»

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 coq.synterp-actions that lists the actions performed so far. The interp phase can use