1. matitaEngine splitted into disambiguation (now in grafite_parser) and

[helm.git] / helm / matita / dump_moo.ml

diff --git a/helm/matita/dump_moo.ml b/helm/matita/dump_moo.ml
index 045a7b91bb456ae60981a6e5065fa7a8d110d76b..cf872bdebcd4c02e812b294a716c1105cd171aa7 100644 (file)
--- a/helm/matita/dump_moo.ml
+++ b/helm/matita/dump_moo.ml
@@ -48,7 +48,7 @@ let _ =
         let commands, metadata = GrafiteMarshal.load_moo ~fname in
         List.iter
           (fun cmd ->
-            printf "  %s\n" (GrafiteAstPp.pp_command cmd); flush stdout)
+            printf "  %s\n" (GrafiteAstPp.pp_cic_command cmd); flush stdout)
           commands;
         List.iter
           (fun m ->