From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 25 Oct 2004 14:33:17 +0000 (+0000)
Subject: bugfix in cmatch constants_no now consider also the number of types of
X-Git-Tag: V_0_0_10~14
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b6658a4a5c874be0223f44c7c1b99900185cbc60;p=helm.git

bugfix in cmatch constants_no now consider also the number of types of
main
---

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index 2e5250f62..3a0b63d9e 100644
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -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