X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FcicNotation.mli;h=9eb98c1d3339ad2ef3142bc30fd7b12196c126d5;hb=9d4a3a25b327bb2c15bd0cff116ba6698b1a4335;hp=1c6e95385a352f67072b094f4b5b677051d30bb5;hpb=9a0e4f3be9f70662f18d2d3b6dd60ae79fba565b;p=helm.git

diff --git a/helm/ocaml/grafite/cicNotation.mli b/helm/ocaml/grafite/cicNotation.mli
index 1c6e95385..9eb98c1d3 100644
--- a/helm/ocaml/grafite/cicNotation.mli
+++ b/helm/ocaml/grafite/cicNotation.mli
@@ -26,13 +26,10 @@
 type notation_id
 
 val process_notation:
-  ('a, 'b) GrafiteAst.command -> ('a, 'b) GrafiteAst.command * notation_id list
+  'obj GrafiteAst.command -> 'obj GrafiteAst.command * notation_id list
 
 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