Exported a couple of functions.

--Thi sline, and those below, will be ignored--

M    metadataQuery.mli

diff --git a/helm/software/components/tactics/metadataQuery.mli b/helm/software/components/tactics/metadataQuery.mli
index a1b5336010d09f982468d0ad5a7b71b872769812..f8559c886490759e3b77eac278fe458aa4cf5ed0 100644 (file)
--- a/helm/software/components/tactics/metadataQuery.mli
+++ b/helm/software/components/tactics/metadataQuery.mli
@@ -38,6 +38,17 @@ val signature_of:
   ProofEngineTypes.goal ->
   MetadataConstraints.UriManagerSet.t
 
+val signature_of_hypothesis:
+  Cic.hypothesis list -> 
+  Cic.metasenv -> 
+  MetadataConstraints.UriManagerSet.t
+
+val close_with_types: 
+  MetadataConstraints.UriManagerSet.t ->
+  Cic.metasenv -> 
+  Cic.context -> 
+  MetadataConstraints.UriManagerSet.t
+
 val universe_of_goal:
   dbd:HSql.dbd -> 
   bool ->  (* apply only or not *)