X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=0b8b58c0ddc1d452cfa2e9f58d2cddb38237e068;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=36f7cda6dc9d059bb22a14324dfbdd3febdc00f5;hpb=779859f7a9e317e378d258897c289f447adea7ad;p=helm.git

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 36f7cda6d..0b8b58c0d 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -29,7 +29,7 @@ open Printf
 
 open GrafiteTypes
 
-exception AttemptToInsertAnAlias of #LexiconEngine.status
+exception AttemptToInsertAnAlias of LexiconEngine.status
 
 let slash_n_RE = Pcre.regexp "\\n" ;;
 
@@ -77,7 +77,7 @@ let dump f =
 	          (Helm_registry.get_bool "matita.paste_unicode_as_tex")
 	 in
          output_string och str
-      | G.Executable (loc, G.Command (_, G.Include (_, false, _))) -> ()
+      | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> ()
       | stm ->
          output_string och (pp_statement stm); nl (); nl ()
    in
@@ -235,7 +235,8 @@ let compile atstart options fname =
       with
       | [] -> grafite_status
       | (g,None)::_ -> g
-      | (g,Some _)::_ -> raise (AttemptToInsertAnAlias g)
+      | (g,Some _)::_ ->
+         raise (AttemptToInsertAnAlias (g :> LexiconEngine.status))
      with MatitaEngine.EnrichedWithStatus 
             (GrafiteEngine.Macro (floc, f), grafite) as exn ->
             match f (get_macro_context (Some grafite)) with 
@@ -273,7 +274,7 @@ let compile atstart options fname =
         (* FG: we do not generate .moo when dumping .mma files *)
         GrafiteMarshal.save_moo moo_fname moo_content_rev;
         LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
-        NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+        NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
          grafite_status#dump
      end;
      let tm = Unix.gmtime elapsed in