]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matitacLib.ml
- hExtlib: new function "list_assoc_all"
[helm.git] / helm / software / matita / matitacLib.ml
index 5a14b2703bc8a24843bb25ff9f3ddda91b6b99a1..489e37c86417bbf9688b9bb816a933b56ff06b27 100644 (file)
@@ -70,10 +70,9 @@ let dump f =
    let nl () =  output_string och (pp_statement nl_ast) in
    MatitaMisc.out_preamble och;
    let grafite_parser_cb status = function
-      | G.Executable (_, G.Macro (_, G.Inline (_, style, uri, prefix, flavour))) ->
+      | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) ->
          let str =
-            ApplyTransformation.txt_of_inline_macro style prefix uri
-               ?flavour
+            ApplyTransformation.txt_of_inline_macro params uri
               ~map_unicode_to_tex:
                  (Helm_registry.get_bool "matita.paste_unicode_as_tex")
         in
@@ -239,7 +238,7 @@ let compile atstart options fname =
      with MatitaEngine.EnrichedWithStatus 
             (GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn ->
             match f (get_macro_context (Some grafite)) with 
-            | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) ->
+            | _, GrafiteAst.Inline (_, _suri, _params) ->
 (*              
              let str =
                ApplyTransformation.txt_of_inline_macro style prefix suri