New tactic: inversion.

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

diff --git a/helm/ocaml/grafite/cicNotation.ml b/helm/ocaml/grafite/cicNotation.ml
index bab8cb97bb5b72a49101512d23bd04e4661ab7df..9500a8e11b3882d90d752a10e07c1ad92e1f49c7 100644 (file)
--- a/helm/ocaml/grafite/cicNotation.ml
+++ b/helm/ocaml/grafite/cicNotation.ml
@@ -36,7 +36,9 @@ let process_notation st =
       let rule_id =
         if dir <> Some `RightToLeft then
           [ RuleId (CicNotationParser.extend l1 ?precedence ?associativity
-              (fun env loc -> TermContentPres.instantiate_level2 env l2)) ]
+              (fun env loc ->
+                CicNotationPt.AttributedTerm
+                 (`Loc loc,TermContentPres.instantiate_level2 env l2))) ]
         else
           []
       in
@@ -59,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) ->