From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 12 Dec 2008 12:11:54 +0000 (+0000)
Subject: added some hardcoded universes, needed to typecheck the librarya
X-Git-Tag: make_still_working~4412
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=87877b88aa97c4de2587b794eedced35d97ec8e4;p=helm.git

added some hardcoded universes, needed to typecheck the librarya
---

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index a09c08599..0efb49bff 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -484,5 +484,16 @@ in
          NCicEnvironment.add_constraint true (mk_type 0) (mk_cprop 1);
          NCicEnvironment.add_constraint false (mk_cprop 0) (mk_type 0);
          NCicEnvironment.add_constraint false (mk_type 0) (mk_cprop 0);
+
+         NCicEnvironment.add_constraint true (mk_type 1) (mk_type 2);
+         NCicEnvironment.add_constraint true (mk_cprop 1) (mk_cprop 2);
+         NCicEnvironment.add_constraint true (mk_cprop 1) (mk_type 2);
+         NCicEnvironment.add_constraint true (mk_type 1) (mk_cprop 2);
+         NCicEnvironment.add_constraint false (mk_cprop 1) (mk_type 1);
+         NCicEnvironment.add_constraint false (mk_type 1) (mk_cprop 1);
+
+         NCicEnvironment.add_constraint false (mk_cprop 2) (mk_type 2);
+         NCicEnvironment.add_constraint false (mk_type 2) (mk_cprop 2);
+
 ;;