- replaced part1a/defn with the version based on induction/inversion and deleted

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

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 6c3749db3e13cca73850b0a9421ccd8e44d5c072..c96fdf82db4a7c8d0793d00ce11d84d78c3f30c8 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -70,14 +70,14 @@ 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
          output_string och str
+      | G.Executable (loc, G.Command (_, G.Include (_, true, _))) -> ()
       | stm ->
          output_string och (pp_statement stm); nl (); nl ()
    in
@@ -239,7 +239,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
@@ -337,7 +337,7 @@ module F =
     let root_and_target_of opts mafile = 
       try
         let include_paths = get_include_paths opts in
-        let root,baseuri,_,_ =
+        let root,baseuri,_,relpath =
           Librarian.baseuri_of_script ~include_paths mafile 
         in
         let obj_writeable, obj_read_only =
@@ -350,8 +350,8 @@ module F =
               LibraryMisc.obj_file_of_baseuri 
                         ~must_exist:false ~baseuri ~writable:false
         in
-        Some root, obj_writeable, obj_read_only
-      with Librarian.NoRootFor x -> None, "", ""
+        Some root, relpath, obj_writeable, obj_read_only
+      with Librarian.NoRootFor x -> None, "", "", ""
     ;;
 
     let mtime_of_source_object s =