X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FbatchParser.mli;h=6d2900304a228708270a8268e1f947c367c13b74;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=edfaa69272d3b032fa1da3604e86db93fde7a7bf;hpb=8eb9b5bc9507708e51c1d2d8616bb7b963aa6ff5;p=helm.git

diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli
index edfaa6927..6d2900304 100644
--- a/helm/gTopLevel/batchParser.mli
+++ b/helm/gTopLevel/batchParser.mli
@@ -39,11 +39,16 @@ 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:
- Mysql.dbd -> ?uri_pred:(string -> bool) -> string ->
-  (DisambiguatingParser.EnvironmentP3.t * Cic.metasenv * Cic.term) list
+ Mysql.dbd -> ?uri_pred:(string -> bool) -> string ->  
+  CicUniv.universe_graph ->
+  (DisambiguatingParser.EnvironmentP3.t * 
+   Cic.metasenv * 
+   Cic.term * 
+   CicUniv.universe_graph) list
 
   (** as above, but instead of returning the parsed cic term, pretty prints it
    * (ignoring returned metasenv)
    *)
-val parse_pp: Mysql.dbd -> ?uri_pred:(string -> bool) -> string -> string list
+val parse_pp: Mysql.dbd -> ?uri_pred:(string -> bool) -> 
+  string -> CicUniv.universe_graph -> string list