From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Dec 2008 20:37:50 +0000 (+0000)
Subject: type3
X-Git-Tag: make_still_working~4347
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a0f3d0aa2cc139a18559d3efbddd2e5f3cdce927;p=helm.git

type3
---

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 9f14c503f..bfe12cee7 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -493,8 +493,15 @@ in
          NCicEnvironment.add_constraint false (mk_cprop 1) (mk_type 1);
          NCicEnvironment.add_constraint false (mk_type 1) (mk_cprop 1);
 
+         NCicEnvironment.add_constraint true (mk_type 2) (mk_type 3);
+         NCicEnvironment.add_constraint true (mk_cprop 2) (mk_cprop 3);
+         NCicEnvironment.add_constraint true (mk_cprop 2) (mk_type 3);
+         NCicEnvironment.add_constraint true (mk_type 2) (mk_cprop 3);
          NCicEnvironment.add_constraint false (mk_cprop 2) (mk_type 2);
          NCicEnvironment.add_constraint false (mk_type 2) (mk_cprop 2);
 
+         NCicEnvironment.add_constraint false (mk_cprop 3) (mk_type 3);
+         NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3);
+
 ;;