X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataExtractor.mli;h=68af269a91a59a8a8e812b8abc78627e28c4f5d9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ce057a85a6c25b50fcc356e7c70871904514a07e;hpb=7403c949ea3a84624f8c05deee00de53336937ba;p=helm.git

diff --git a/helm/ocaml/metadata/metadataExtractor.mli b/helm/ocaml/metadata/metadataExtractor.mli
index ce057a85a..68af269a9 100644
--- a/helm/ocaml/metadata/metadataExtractor.mli
+++ b/helm/ocaml/metadata/metadataExtractor.mli
@@ -23,14 +23,20 @@
  * 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
 
-val compute_term:
-  MetadataTypes.position -> Cic.term ->
-    MetadataTypes.metadata list
+  (** 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