* http://helm.cs.unibo.it/
*)
-val compute: body:Cic.term option -> ty:Cic.term -> MetadataTypes.metadata list
+val compute:
+ body:Cic.term option ->
+ ty:Cic.term ->
+ MetadataTypes.metadata list
- (** @return tuples <uri, name, metadata> *)
-val compute_ind:
- uri:UriManager.uri -> types:Cic.inductiveType list ->
- (string * string * MetadataTypes.metadata list) list
+ (** @return tuples <uri, shortname, metadata> *)
+val compute_obj:
+ UriManager.uri ->
+ (UriManager.uri * string * MetadataTypes.metadata list) 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