1. Several files in grafite that should be in grafite_parser moved there.

[helm.git] / helm / ocaml / grafite / cicNotation.mli

diff --git a/helm/ocaml/grafite/cicNotation.mli b/helm/ocaml/grafite/cicNotation.mli
index 1c6e95385a352f67072b094f4b5b677051d30bb5..41b775562d43557a151a96ecc07bf962bd2e33c0 100644 (file)
--- a/helm/ocaml/grafite/cicNotation.mli
+++ b/helm/ocaml/grafite/cicNotation.mli
@@ -30,9 +30,6 @@ val process_notation:
 
 val remove_notation: notation_id -> unit
 
-(** @param fname file from which load notation *)
-val load_notation: string -> unit
-
 (** {2 Notation enabling/disabling}
  * Right now, only disabling of notation during pretty printing is supporting.
  * If it is useful to disable it also for the input phase is still to be