parameter sintax added to axiom statement

[helm.git] / helm / software / components / grafite_parser / cicNotation2.mli

diff --git a/helm/software/components/grafite_parser/cicNotation2.mli b/helm/software/components/grafite_parser/cicNotation2.mli
index 972c55b513c93e7f3a25cdd86573471b8e04db7c..6c9c44167256b8e2da2fe063941a4e4ed2aabedb 100644 (file)
--- a/helm/software/components/grafite_parser/cicNotation2.mli
+++ b/helm/software/components/grafite_parser/cicNotation2.mli
@@ -23,14 +23,7 @@
  * 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:
- include_paths:string list ->
- string ->
-  Cic.term DisambiguateTypes.environment * 
-  Cic.term DisambiguateTypes.multiple_environment
-
 (** @param fname file from which load notation *)
-val load_notation: include_paths:string list -> string -> LexiconEngine.status
+val load_notation:
+ #LexiconEngine.status as 'status -> include_paths:string list -> string ->
+  'status