aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/proof-engine
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-04-27 01:39:39 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-09 10:35:05 +0200
commit5daa99eba8cf14209556bf739e4c0807be25236b (patch)
treedaf52dd95104991fd10cf1a8ae407f9b8c24a5e9 /doc/sphinx/proof-engine
parentc8f204caf9d753993e9bf7517bb78abc3478c933 (diff)
A few fixes in chapter tactics.
Diffstat (limited to 'doc/sphinx/proof-engine')
-rw-r--r--doc/sphinx/proof-engine/tactics.rst6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index b3537bad8..1ae9e3c72 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -503,7 +503,7 @@ Applying theorems
.. tacv:: eapply {+, @term with @bindings_list} in @ident as @intro_pattern.
- This works as :tacn:`apply ... in as` but using ``eapply``.
+ This works as :tacn:`apply ... in ... as` but using ``eapply``.
.. tacv:: simple apply @term in @ident
@@ -518,8 +518,8 @@ Applying theorems
.. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern}
.. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern}
- This summarizes the different syntactic variants of :n:`apply @term in
- @ident` and :n:`eapply @term in @ident`.
+ This summarizes the different syntactic variants of :n:`apply @term in @ident`
+ and :n:`eapply @term in @ident`.
.. tacn:: constructor @num
:name: constructor