Huge reorganization of matita and ocaml.

[helm.git] / helm / ocaml / grafite_parser / cicNotation2.mli

diff --git a/helm/ocaml/grafite_parser/cicNotation2.mli b/helm/ocaml/grafite_parser/cicNotation2.mli
index 2d8c4b3c8f78de176e3a34b15d28bf71051d616f..00f184b3bf192eeee0f724277711e1e42cdb8f00 100644 (file)
--- 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