]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/filter_auto.mli
New filtering function for "Auto" tactic using "just costraints"
[helm.git] / helm / ocaml / tactics / filter_auto.mli
index 44dfd32a9d2352095a50e64589b3685f2ef4bf46..06909a836ea1aa57c6476f9a92b1d7cf7ad7ef75 100644 (file)
@@ -23,7 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-
+val power:
+ int -> int -> int 
 
 val filter_new_constants: 
        Mysql.dbd ->
@@ -31,3 +32,8 @@ val filter_new_constants:
        int * string ->
        bool
 
+val filter_uris:
+       Mysql.dbd ->
+       NewConstraints.StringSet.t ->
+       (int * string) list ->
+       (int * string) list