From 0db291bf647ae5d8aa54c58691ab170b46e7666a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 29 Oct 2009 16:52:06 +0000 Subject: [PATCH] For some obscure reason, more universes are now needed (but not used in scripts). To be better understood. --- helm/software/matita/contribs/ng_assembly/common/theory.ma | 2 ++ 1 file changed, 2 insertions(+) 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 *) -- 2.39.5