callbacks were taking in input a status bu were not using them.

[helm.git] / helm / software / matita / matitacLib.ml

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index b3b95325acc8a66ec7fc7e6c5237538975fb7078..baac2409cf1a3243cd5833ffb7ddd81091bf7061 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -69,7 +69,7 @@ let dump f =
    let och = open_out f in
    let nl () =  output_string och (pp_statement nl_ast) in
    MatitaMisc.out_preamble och;
-   let grafite_parser_cb status = function
+   let grafite_parser_cb = function
       | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) ->
          let str =
             ApplyTransformation.txt_of_inline_macro params uri
@@ -81,7 +81,7 @@ let dump f =
       | stm ->
          output_string och (pp_statement stm); nl (); nl ()
    in
-   let lexicon_parser_cb status cmd =
+   let lexicon_parser_cb cmd =
          output_string och (pp_lexicon cmd); nl (); nl ()
    in
    begin fun () ->
@@ -91,8 +91,8 @@ let dump f =
    end, 
    begin fun x ->
       close_out och;
-      GrafiteParser.set_grafite_callback (fun _ _ -> ());
-      GrafiteParser.set_lexicon_callback (fun _ _ -> ());
+      GrafiteParser.set_grafite_callback (fun _ -> ());
+      GrafiteParser.set_lexicon_callback (fun _ -> ());
       Helm_registry.set_bool "matita.moo" true;
       x
    end