From 1624735620d7e375a124231fea94648eac0da342 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 5 Aug 2014 14:50:04 +0200
Subject: Documentation of [uconstr]: typesetting.

---
 doc/refman/RefMan-ltac.tex | 9 ++++-----
 1 file 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}
-- 
cgit v1.2.3