X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fmetadata%2FmetadataConstraints.ml;h=6cab493fce46d067aa46c33f93d58d27e0a5d7f7;hb=da415a61eb8ecfc58817196363fad86b35efe490;hp=07fcc738b0b2fee951580106307200b4823f505c;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/metadata/metadataConstraints.ml b/components/metadata/metadataConstraints.ml
index 07fcc738b..6cab493fc 100644
--- a/components/metadata/metadataConstraints.ml
+++ b/components/metadata/metadataConstraints.ml
@@ -384,7 +384,7 @@ let rec signature_of = function
       Some (u, []), add l
   | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
       let suri = UriManager.uri_of_uriref u t None in
-      if u = HelmLibraryObjects.Logic.eq_URI then
+       if LibraryObjects.is_eq_URI u then 
 	  (* equality is handled in a special way: in particular, 
              the type, if defined, is always added to the prefix, 
 	     and n is not decremented - it should have been n-2 *)
@@ -400,7 +400,7 @@ let rec signature_of = function
             let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in
 	    let inconcl =  UriManagerSet.remove suri1 (add l1) in
             Some (suri, [suri1]), inconcl
-	| _ :: _ -> Some (suri, []), UriManagerSet.empty
+	| _ :: tl -> Some (suri, []), add tl
 	| _ -> assert false (* args number must be > 0 *)
       else
 	Some (suri, []), add l
@@ -541,7 +541,7 @@ let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
             List.map (fun uri -> (card, uri)) res))
           maximal_prefixes)
     in
-    Printf.fprintf stderr "all: %d\n" (List.length all);flush_all ();
+(*     Printf.fprintf stderr "all: %d\n" (List.length all);flush_all (); *)
     List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
   let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
     greater_than @ equal_to