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

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

diff --git a/helm/ocaml/grafite/cicNotation.ml b/helm/ocaml/grafite/cicNotation.ml
index 30dd5f4d191d3cdc071f50fb855c92ac9f96d04c..9500a8e11b3882d90d752a10e07c1ad92e1f49c7 100644 (file)
--- 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) ->