X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=bfe12cee70bf5174000fd9cd44ed6a539a43d1bc;hb=06585b97fad3158391dbbea1fcad5866f5269eee;hp=9f14c503f3bc30a99cb9ae29457e7ecb345645ff;hpb=f2e2d1f6cccad2cc1ce70ef7fa2841cf0a457953;p=helm.git

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);
+
 ;;