fix doc generation

examples/tutorial_coq_elpi_HOAS.v

@@ -580,13 +580,13 @@ 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{Coq-Elpi mapping:*[?]X12 <-> X1*}
+.. mquote:: .s(Elpi).msg{Coq-Elpi mapping:*[?]X11 <-> X1*}
    :language: text
 
 Note that Coq's evar identifiers are of the form `?X<n>`, while the Elpi ones
-have no leading `?`. The Coq Evar map says that `?X12` has type `nat`:
+have no leading `?`. The Coq Evar map says that `?X11` has type `nat`:
 
-.. mquote:: .s(Elpi).msg{EVARS:*[?]X12==[[] |- nat[]]*}
+.. mquote:: .s(Elpi).msg{EVARS:*[?]X11==[[] |- nat[]]*}
    :language: text
 
 The intuition is that Coq's Evar map (AKA sigma or evd), which assigns
@@ -631,12 +631,12 @@ conclusion (the suspended goal).
  
 The mapping between Coq and Elpi is:
 
-.. mquote:: .s(Elpi).msg{Coq-Elpi mapping:*[?]X15 <-> X1*}
+.. mquote:: .s(Elpi).msg{Coq-Elpi mapping:*[?]X13 <-> X1*}
    :language: text
 
 where `?X13` can be found in Coq's sigma:
 
-.. mquote:: .s(Elpi).msg{EVARS:*[?]X15==[[]x |- nat[]]*}
+.. mquote:: .s(Elpi).msg{EVARS:*[?]X13==[[]x |- nat[]]*}
    :language: text
 
 As expected both Elpi's constraint and Coq's evar map record a context