Apply suggestions from code review

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
SkySkimmer · Oct 11, 2023 · cc8130e · cc8130e
1 parent cbdbaaf
commit cc8130e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
@@ -352,11 +352,11 @@ Printing Ltac2 tactics
 
 .. cmd:: Ltac2 Globalize @ltac2_expr
 
-   This command prints the result of resolving notations in the given expression.
+   Prints the result of resolving notations in the given expression.
 
 .. cmd:: Ltac2 Check @ltac2_expr
 
-   This command typechecks the given expression and prints the result.
+   Typechecks the given expression and prints the result.
 
 .. cmd:: Print Ltac2 Signatures