diff --git a/tutorial_coq_elpi_command.html b/tutorial_coq_elpi_command.html index fa047d363..aa76c0239 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.Module23»

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

The module is «tutorial_coq_elpi_command.Module71»

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 diff --git a/tutorial_elpi_lang.html b/tutorial_elpi_lang.html index 5daa7f008..75ef63813 100644 --- a/tutorial_elpi_lang.html +++ b/tutorial_elpi_lang.html @@ -1258,7 +1258,7 @@

Trace browser

rid:1 step:2 gid:16 user:subgoal = 18
rid:1 step:2 gid:18 user:newgoal = pi c0 \ of c0 X1 => of (app c0 c0) X2
rid:1 step:2 gid:18 user:rule:backchain = success -
}}} -> (0.001s)
run 3 {{{ +
}}} -> (0.000s)
run 3 {{{
rid:1 step:3 gid:18 user:curgoal = pi pi c0 \ of c0 X1 => of (app c0 c0) X2
rid:1 step:3 gid:18 user:rule = pi @@ -1303,7 +1303,7 @@

Trace browser

.X5
rid:1 step:6 gid:0 user:assign = X1 := arr X5 X2
rid:1 step:6 gid:21 user:rule:backchain = success -
}}} -> (0.001s)
run 7 {{{ +
}}} -> (0.000s)
run 7 {{{
rid:1 step:7 gid:22 user:curgoal = of of c0 X5
rid:1 step:7 gid:22 user:rule = backchain