X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=bfe12cee70bf5174000fd9cd44ed6a539a43d1bc;hb=8b7ad9b29b3448b72e476ba077e2d0faad86c058;hp=a09c085995108286f62dea5db8c6c36706e3140d;hpb=266fe24a5a5548c30f597ccd38578877643404d3;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index a09c08599..bfe12cee7 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -40,7 +40,8 @@ let refine_term
         assert false
     in
     let metasenv, subst, term, _ = 
-      NCicRefiner.typeof 
+      NCicRefiner.typeof
+        (NCicUnifHint.db ())
         ~look_for_coercion:(
           if use_coercions then 
            NCicCoercion.look_for_coercion coercion_db
@@ -484,5 +485,23 @@ 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 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);
+
 ;;