]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/mquery.mli
New module helm-mathql.
[helm.git] / helm / gTopLevel / mquery.mli
index 3ea31b8d214585ed73f15b32cc27d745fcb11153..2d07f4ec491d82b196f421972e4b06bd0fdd9531 100644 (file)
 (*                                                                            *)
 (******************************************************************************)
 
-val str_tref  : Mathql.mqtref -> string        (* string linearization of a tokenized reference *)
-
-val out_query : Mathql.mquery -> string        (* HTML representation of a query *)
-
-val tref_uref : Mathql.mquref -> Mathql.mqtref (* "tref of uref" conversion *)
-
 val init      : unit -> unit                   (* INIT database function *)
 
 val close     : unit -> unit                   (* CLOSE database function *)