diff options
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 8c5eee7f4e..49b0cadf05 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -893,11 +893,10 @@ using Ltac with the syntax \end{quote} An untyped term, in Ltac, can contain references to hypotheses or to -Ltac variables containing typed or untyped terms. - -A untyped term can be type-checked using the function {\tt type\_term} -whose argument is parsed as an untyped term and returns a well-typed -term which can be used in tactics. +Ltac variables containing typed or untyped terms. An untyped term can +be type-checked using the function {\tt type\_term} whose argument is +parsed as an untyped term and returns a well-typed term which can be +used in tactics. \begin{quote} {\tt type\_term} {\term} |