From e9eda8f13045ff3d4f7b1ec93dec96e09bf65f1a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 8 Jul 2009 09:58:29 +0000 Subject: [PATCH] removed useless universes --- helm/software/matita/tests/esempio_oliboni.ma | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/helm/software/matita/tests/esempio_oliboni.ma b/helm/software/matita/tests/esempio_oliboni.ma index aca01514d..8eb612e4e 100644 --- a/helm/software/matita/tests/esempio_oliboni.ma +++ b/helm/software/matita/tests/esempio_oliboni.ma @@ -18,13 +18,10 @@ include "nat/nat.ma". universe constraint Type[0] < Type[1]. universe constraint Type[1] < Type[2]. universe constraint CProp[0] < CProp[1]. -universe constraint CProp[1] < CProp[2]. universe constraint Type[0] ≤ CProp[0]. universe constraint CProp[0] ≤ Type[0]. universe constraint Type[1] ≤ CProp[1]. universe constraint CProp[1] ≤ Type[1]. -universe constraint Type[2] ≤ CProp[2]. -universe constraint CProp[2] ≤ Type[2]. ninductive A : Type[0] ≝ | K : nat → A @@ -62,4 +59,4 @@ ncases a; ncases b; - \ No newline at end of file + -- 2.39.5