The regression tests now check also the generated disambiguation environments.

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

diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli
index ff82e6fa057d9001dc43e4241d5e0a03df0640f1..9ba49ef52b9ff80b11b1c9dfce55727b3de67dd1 100644 (file)
--- a/helm/gTopLevel/batchParser.mli
+++ b/helm/gTopLevel/batchParser.mli
@@ -37,7 +37,9 @@ val uri_pred_of_conf: bool -> string -> (string -> bool)
    * batch mode if possible, otherwise raises Failure above.
    * 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 -> (Cic.metasenv * Cic.term) list
+val parse:
+ MQIConn.handle -> ?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)