ported to Mysql

[helm.git] / helm / gTopLevel / batchParser.mli

diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli
index b6410fe3bc1af096d6e6b8ae4c1c9847c9e9a989..edfaa69272d3b032fa1da3604e86db93fde7a7bf 100644 (file)
--- a/helm/gTopLevel/batchParser.mli
+++ b/helm/gTopLevel/batchParser.mli
@@ -39,11 +39,11 @@ val uri_pred_of_conf:
    * uri_pred is the predicate used to select which uris are tried. Per default
    * only constant URIs are accepted *)
 val parse:
- MQIConn.handle -> ?uri_pred:(string -> bool) -> string ->
+ Mysql.dbd -> ?uri_pred:(string -> bool) -> string ->
   (DisambiguatingParser.EnvironmentP3.t * Cic.metasenv * Cic.term) list
 
   (** as above, but instead of returning the parsed cic term, pretty prints it
    * (ignoring returned metasenv)
    *)
-val parse_pp: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> string list
+val parse_pp: Mysql.dbd -> ?uri_pred:(string -> bool) -> string -> string list