From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 18 Feb 2004 13:17:52 +0000 (+0000)
Subject: now mathql interpreter use helm registry
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=refs%2Fheads%2Funlabeled-1.1.2

now mathql interpreter use helm registry
---

diff --git a/helm/ocaml/mathql_interpreter/mQIMap.mli b/helm/ocaml/mathql_interpreter/mQIMap.mli
index bf78f6d62..50f5bb0fa 100644
--- a/helm/ocaml/mathql_interpreter/mQIMap.mli
+++ b/helm/ocaml/mathql_interpreter/mQIMap.mli
@@ -32,9 +32,9 @@ type pg_tables
 
 type pg_alias
 
-val empty_map     : unit -> string * pg_map * pg_alias
+val empty_map     : unit -> pg_map * pg_alias
 
-val read_map      : unit -> string * pg_map * pg_alias
+val read_map      : unit -> pg_map * pg_alias
 
 val get_tables    : pg_map -> MathQL.path -> pg_tables