]> matita.cs.unibo.it Git - helm.git/commitdiff
bugfix in cmatch constants_no now consider also the number of types of
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 25 Oct 2004 14:33:17 +0000 (14:33 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 25 Oct 2004 14:33:17 +0000 (14:33 +0000)
main

helm/ocaml/metadata/metadataConstraints.ml

index 2e5250f6208df28f07346803fa60d97c598eacf6..3a0b63d9e5f5948d9fc21b7178b4de68dfaa3e52 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
@@ -481,7 +482,7 @@ let cmatch ~(dbh:Dbi.connection) t =
            to apply the only constraints *)
         let prefixes =
           if constants_no = 0 then
-            Some main, [0, []; List.length types, types]
+            Some main, [0, []; types_no, types]
           else
             prefixes constants_no t
         in