]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataConstraints.mli
added rating parameter to at_least (used by elim)
[helm.git] / helm / ocaml / metadata / metadataConstraints.mli
index 48143490ff1682d3240d25eaa4781ba80bf4dd15..ddf672b7f1d939d84099c216bbd3116190b9afcb 100644 (file)
@@ -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