From 951069678fea0d6dcdde984320ec5057ddc57c3c Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 1 Feb 2006 23:12:00 +0000
Subject: [PATCH] line breaking

---
 helm/papers/matita/matita2.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index d902d1380..a0c014251 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1578,7 +1578,8 @@ where \texttt{H} is $\beta$-expanded over the second \texttt{n}
 occurrence. 
 
 At this point, since \COQ{} unification algorithm is essentially first-order,
-the application of an elimination principle (a term with type $\forall P.\forall
+the application of an elimination principle (a term of type\linebreak
+$\forall P.\forall
 x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with
 \texttt{(fun n0: nat => m + n = n0)}.
 
-- 
2.39.5