added filtering criteria on differences between number of constants in

[helm.git] / helm / ocaml / metadata / metadataExtractor.mli

diff --git a/helm/ocaml/metadata/metadataExtractor.mli b/helm/ocaml/metadata/metadataExtractor.mli
index ce057a85a6c25b50fcc356e7c70871904514a07e..450c3a525cea62f26d0f397bbe6fe7655fe02785 100644 (file)
--- a/helm/ocaml/metadata/metadataExtractor.mli
+++ b/helm/ocaml/metadata/metadataExtractor.mli
@@ -34,3 +34,10 @@ val compute_term:
   MetadataTypes.position -> Cic.term ->
     MetadataTypes.metadata list
 
+module IntSet: Set.S with type elt = int
+
+  (** given a term, returns a pair of sets corresponding respectively to the set
+    * of meta numbers occurring in term's conclusion and the set of meta numbers
+    * occurring in term's hypotheses *)
+val compute_metas: Cic.term -> IntSet.t * IntSet.t
+