From: Ferruccio Guidi 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/?a=commitdiff_plain;h=ddf599524a4324cbd5e20d2ed6ed6821ac7b75c8;p=helm.git 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