Doc: Renaming an old-style numerical evar in an alphabetical one.

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 19ab786d1..20a362c4c 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -511,8 +511,8 @@ Applying theorems
    on subterms that contain no variables to instantiate. For instance, if
    :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and
    :g:`H0 : O = O` then ``simple apply H in H0`` does not succeed because it
-   would require the conversion of :g:`id ?1234` and :g:`O` where :g:`?1234` is
-   a variable to instantiate. Tactic :n:`simple apply @term in @ident` does not
+   would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is
+   an existential variable to instantiate. Tactic :n:`simple apply @term in @ident` does not
    either traverse tuples as :n:`apply @term in @ident` does.
 
 .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern}