snapshot, still work in progress

[helm.git] / helm / ocaml / metadata / metadataExtractor.mli

diff --git a/helm/ocaml/metadata/metadataExtractor.mli b/helm/ocaml/metadata/metadataExtractor.mli
index ef7ea763c6f912afe90aa448b85c00623b36a126..ce057a85a6c25b50fcc356e7c70871904514a07e 100644 (file)
--- 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
+