diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-25 21:24:37 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-11 18:54:24 +0200 |
commit | 9b070738af8fbfb6f76f2963c630414a76817852 (patch) | |
tree | 73fce9184250144963a3c66af7ba05c1bcd06183 /doc | |
parent | 8f18af6f61f70c0d566bcaba5f8d285e77601f5a (diff) |
Doc: Renaming an old-style numerical evar in an alphabetical one.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 4 |
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} |