]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/dump_moo.ml
updating the structures for sorts
[helm.git] / helm / software / matita / dump_moo.ml
index 54eaea4bae87a8e27ce33e56b19ea0246eb523bb..6b8658abdba777d7376163576f41db7a29304fae 100644 (file)
@@ -52,8 +52,8 @@ let _ =
           (fun cmd ->
             printf "  %s\n%!"
               (GrafiteAstPp.pp_command
-                ~term_pp:(fun _ -> assert false)
-                ~obj_pp:(fun _ -> assert false) cmd))
+                ~term_pp:(fun t -> CicPp.ppterm t)
+                ~obj_pp:(fun _ -> "OBJ") cmd))
           commands;
       end)
     (List.rev !moos)