]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/metadata/metadataExtractor.mli
ocaml 3.09 transition
[helm.git] / helm / ocaml / metadata / metadataExtractor.mli
index 450c3a525cea62f26d0f397bbe6fe7655fe02785..68af269a91a59a8a8e812b8abc78627e28c4f5d9 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
-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
-
-val compute_term:
-  MetadataTypes.position -> Cic.term ->
+val compute: 
+  body:Cic.term option -> 
+  ty:Cic.term -> 
     MetadataTypes.metadata 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