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 31cb11c9ce0ccd06b0f587f8625f1b65a0e1441a..b6a84d6af9dcff803e6da3e03206505ed634446d 100644 (file)
--- 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 *)