From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 29 Oct 2008 15:18:35 +0000 (+0000)
Subject: Exported a couple of functions.
X-Git-Tag: make_still_working~4614
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5641b3c51a2ed61a0635dfbca663b123c417732e;p=helm.git

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 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 *)