From 5641b3c51a2ed61a0635dfbca663b123c417732e Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 29 Oct 2008 15:18:35 +0000
Subject: [PATCH] Exported a couple of functions. --Thi sline, and those below,
 will be ignored--

M    metadataQuery.mli
---
 helm/software/components/tactics/metadataQuery.mli | 11 +++++++++++
 1 file changed, 11 insertions(+)

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