X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FcicNotation.ml;h=9500a8e11b3882d90d752a10e07c1ad92e1f49c7;hb=b92a0ec32215eea5e0452154da54d5a29a84a53e;hp=30dd5f4d191d3cdc071f50fb855c92ac9f96d04c;hpb=019d5023aefd04aff9ac0849405306612d54ba64;p=helm.git

diff --git a/helm/ocaml/grafite/cicNotation.ml b/helm/ocaml/grafite/cicNotation.ml
index 30dd5f4d1..9500a8e11 100644
--- a/helm/ocaml/grafite/cicNotation.ml
+++ b/helm/ocaml/grafite/cicNotation.ml
@@ -61,17 +61,6 @@ let remove_notation = function
   | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
   | InterpretationId id -> TermAcicContent.remove_interpretation id
 
-let load_notation fname =
-  let ic = open_in fname in
-  let lexbuf = Ulexing.from_utf8_channel ic in
-  try
-    while true do
-      match GrafiteParser.parse_statement lexbuf with
-      | Executable (_, Command (_, cmd)) -> ignore (process_notation cmd)
-      | _ -> ()
-    done
-  with End_of_file -> close_in ic
-
 let get_all_notations () =
   List.map
     (fun (interp_id, dsc) ->