Merge pull request #875 from LPCIC/doc

fix doc

Author: gares

.github/workflows/doc.yml

@@ -37,7 +37,6 @@ jobs:
         opam install coq-serapi.8.20.0+0.20.0 ./rocq-elpi.opam coq-core.8.20.0
         sudo apt-get update
         sudo apt-get install python3-pip -y
-        pip3 install git+https://github.com/cpitclaudel/alectryon.git@c8ab1ec
 
     - name: build doc
       run: |

Makefile

@@ -90,9 +90,11 @@ examples-stdlib: theories-stdlib/dune
 
 doc: build
 	@echo "########################## generating doc ##########################"
+	@python3 -m venv alectryon
+	@alectryon/bin/pip3 install git+https://github.com/cpitclaudel/alectryon.git@c8ab1ec
 	@mkdir -p doc
 	@$(foreach tut,$(wildcard examples/tutorial*$(ONLY)*.v),\
-		echo ALECTRYON $(tut) && OCAMLPATH=$(shell pwd)/_build/install/default/lib ./etc/alectryon_elpi.py \
+		echo ALECTRYON $(tut) && OCAMLPATH=$(shell pwd)/_build/install/default/lib alectryon/bin/python3 etc/alectryon_elpi.py \
 		    --frontend coq+rst \
 			--output-directory doc \
 		    --pygments-style vs \

examples/tutorial_coq_elpi_HOAS.v

@@ -578,16 +578,16 @@ Before the call to :builtin:`coq.typecheck`, :builtin:`coq.sigma.print`
 prints nothing interesting, while after the call it also prints the following
 syntactic constraint:
 
-.. mquote:: .s(Elpi).msg(suspended on X1)
+.. mquote:: .s(Elpi).msg(suspended on X0)
    :language: elpi
 
-which indicates that the hole :e:`X1` is linked to a Coq evar
+which indicates that the hole :e:`X0` is linked to a Coq evar
 and is expected to have type `nat`.
 
 Now the bijective mapping from Coq evars to Elpi's unification variables
 is not empty anymore:
 
-.. mquote:: .s(Elpi).msg{Rocq-Elpi mapping:*[?]X11 <-> X1*}
+.. mquote:: .s(Elpi).msg{Rocq-Elpi mapping:*[?]X11 <-> X0*}
    :language: text
 
 Note that Coq's evar identifiers are of the form `?X<n>`, while the Elpi ones
@@ -603,7 +603,7 @@ the same piece of info.
 Naked Elpi unification variables, when passed to Coq's API, are
 automatically linked to a Coq evar. We postpone the explanation of the
 difference "raw" and "elab" unification variables to the chapter about
-tactics, here the second copy of :e:`X1` in the evar constraint plays
+tactics, here the second copy of :e:`X0` in the evar constraint plays
 no role.
 
 Now, what about the typing context?