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=0efb49bff54f039f92b3ff1bbef997fe9091777b;hpb=87877b88aa97c4de2587b794eedced35d97ec8e4;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 0efb49bff..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
@@ -492,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);
+
 ;;