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

diff --git a/helm/ocaml/metadata/metadataExtractor.mli b/helm/ocaml/metadata/metadataExtractor.mli
index ef7ea763c..ce057a85a 100644
--- a/helm/ocaml/metadata/metadataExtractor.mli
+++ b/helm/ocaml/metadata/metadataExtractor.mli
@@ -30,3 +30,7 @@ val compute_ind:
   uri:UriManager.uri -> types:Cic.inductiveType list ->
     (string * string * MetadataTypes.metadata list) list
 
+val compute_term:
+  MetadataTypes.position -> Cic.term ->
+    MetadataTypes.metadata list
+