]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataConstraints.ml
renamed Http_client to Http_user_agent to avoid clashes with Gerd's
[helm.git] / helm / ocaml / metadata / metadataConstraints.ml
index 2e5250f6208df28f07346803fa60d97c598eacf6..fb782494a6a0c99318a9850a991260b6040f9be1 100644 (file)
@@ -466,7 +466,8 @@ let cmatch ~(dbh:Dbi.connection) t =
   | None -> []
   | Some (main, types) ->
       (* the type of eq is not counted in constants_no *)
-      let constants_no = StringSet.cardinal constants in
+      let types_no = List.length types in
+      let constants_no = StringSet.cardinal constants + types_no in
       if (constants_no > critical_value) then 
         let prefixes = prefixes just_factor t in
         (match prefixes with
@@ -480,8 +481,8 @@ let cmatch ~(dbh:Dbi.connection) t =
         (* in this case we compute all prefixes, and we do not need
            to apply the only constraints *)
         let prefixes =
-          if constants_no = 0 then
-            Some main, [0, []; List.length types, types]
+          if constants_no = types_no then
+            Some main, [0, []; types_no, types]
           else
             prefixes constants_no t
         in