X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_parser%2FcicNotation2.mli;h=00f184b3bf192eeee0f724277711e1e42cdb8f00;hb=57d038849d866853795522e360723a881c2d4831;hp=2d8c4b3c8f78de176e3a34b15d28bf71051d616f;hpb=a696aae5ea794cd43fd3d83d37a0345d2a1387b3;p=helm.git

diff --git a/helm/ocaml/grafite_parser/cicNotation2.mli b/helm/ocaml/grafite_parser/cicNotation2.mli
index 2d8c4b3c8..00f184b3b 100644
--- a/helm/ocaml/grafite_parser/cicNotation2.mli
+++ b/helm/ocaml/grafite_parser/cicNotation2.mli
@@ -23,9 +23,13 @@
  * http://helm.cs.unibo.it/
  *)
 
+(** Note: notation is also loaded, but it cannot be undone since the
+    notation_ids part of the status is thrown away;
+    so far this function is useful only in Whelp *)
 val parse_environment:
-  string ->
-   DisambiguateTypes.environment * DisambiguateTypes.multiple_environment
+ include_paths:string list ->
+ string ->
+  DisambiguateTypes.environment * DisambiguateTypes.multiple_environment
 
 (** @param fname file from which load notation *)
-val load_notation: string -> unit
+val load_notation: include_paths:string list -> string -> LexiconEngine.status