Documentation of [uconstr]: typesetting.

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}