X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=4cb18817012d7fb6de7f5432668cddeb494447f8;hb=186638106f23401e88e512a4a6dfd07d73d8be04;hp=f544d8daeed54aad2216322cc09f344e6bfacfa8;hpb=bd1e80fb01cfb419e256d5899ac5bf8818f11e64;p=helm.git

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index f544d8dae..4cb188170 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -53,15 +53,15 @@ let logger =
 
 let mk_type n = 
   if n = 0 then
-     [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+     [`Type, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-     [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+     [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 let mk_cprop n = 
   if n = 0 then 
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 
@@ -151,16 +151,9 @@ let _ =
     try
     let rec aux = function
       | a::(b::_ as tl) ->
-         NCicEnvironment.add_constraint true (mk_type a) (mk_type b);
-         NCicEnvironment.add_constraint true (mk_cprop a) (mk_cprop b);
-         NCicEnvironment.add_constraint true (mk_cprop a) (mk_type b);
-         NCicEnvironment.add_constraint true (mk_type a) (mk_cprop b);
-         NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
-         NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
+         NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b);
+         NCicEnvironment.add_lt_constraint (mk_cprop a) (mk_cprop b);
          aux tl
-      | [a] -> 
-         NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
-         NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
       | _ -> ()
     in
        aux lll