From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 29 Oct 2009 16:52:06 +0000 (+0000)
Subject: For some obscure reason, more universes are now needed (but not used in
X-Git-Tag: make_still_working~3228
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0db291bf647ae5d8aa54c58691ab170b46e7666a;p=helm.git

For some obscure reason, more universes are now needed (but not used in
scripts). To be better understood.
---

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index 31cb11c9c..b6a84d6af 100644
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -21,6 +21,8 @@
 (* ********************************************************************** *)
 
 universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+universe constraint Type[2] < Type[3].
 
 (* ********************************** *)
 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)