+
+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