]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_disambiguation/nCicDisambiguate.ml
More re-working.
[helm.git] / helm / software / components / ng_disambiguation / nCicDisambiguate.ml
index 9f14c503f3bc30a99cb9ae29457e7ecb345645ff..bfe12cee70bf5174000fd9cd44ed6a539a43d1bc 100644 (file)
@@ -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);
+
 ;;