X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FmetadataQuery.mli;h=f8559c886490759e3b77eac278fe458aa4cf5ed0;hb=d0e97750e19af9286400a3e7b161a1c658684848;hp=a1b5336010d09f982468d0ad5a7b71b872769812;hpb=ac741958783108ff31552e533c853e85c2ebb1c5;p=helm.git

diff --git a/helm/software/components/tactics/metadataQuery.mli b/helm/software/components/tactics/metadataQuery.mli
index a1b533601..f8559c886 100644
--- 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 *)