X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.mli;h=ddf672b7f1d939d84099c216bbd3116190b9afcb;hb=88a07a009adcd5c2320900ea342d7682ada587ce;hp=48143490ff1682d3240d25eaa4781ba80bf4dd15;hpb=20054808327ccec9d018b8cc54b31ccb44724f49;p=helm.git

diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli
index 48143490f..ddf672b7f 100644
--- a/helm/ocaml/metadata/metadataConstraints.mli
+++ b/helm/ocaml/metadata/metadataConstraints.mli
@@ -59,6 +59,10 @@ type cardinality_condition =
   | Gt of int
   | Lt of int
 
+type rating_criterion =
+  [ `Hits   (** order by number of hits, most used objects first *)
+  ]
+
   (** @param concl_card cardinality condition on conclusion only
   * @param full_card cardinality condition on the whole statement
   * @param diff required difference between the number of different constants in
@@ -69,6 +73,7 @@ val at_least:
   ?concl_card:cardinality_condition ->
   ?full_card:cardinality_condition ->
   ?diff:cardinality_condition ->
+  ?rating:rating_criterion ->
   MetadataTypes.constr list ->
     string list