Big bug fixed: batchParser applied the varsprefix prefix also to

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

diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli
index 9ba49ef52b9ff80b11b1c9dfce55727b3de67dd1..b6410fe3bc1af096d6e6b8ae4c1c9847c9e9a989 100644 (file)
--- a/helm/gTopLevel/batchParser.mli
+++ b/helm/gTopLevel/batchParser.mli
@@ -26,12 +26,13 @@
 exception Failure of string
 
   (** uri_pred which rejects ll .var URIs *)
-val constants_only: (string -> bool)
+val constants_only: prefix:string -> (string -> bool)
 
   (** @param variables enabled
-   * @param variables prefix
+   * @param variables prefix varsprefix
    * @return uri predicate suitable for functions below *)
-val uri_pred_of_conf: bool -> string -> (string -> bool)
+val uri_pred_of_conf:
+ bool -> prefix:string -> varsprefix:string -> (string -> bool)
 
   (** Parse a cic term from the given string using disambiguating parser in
    * batch mode if possible, otherwise raises Failure above.