X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Fmatita.ml;h=0086f6aeac3f5a48860d13f358837191ee4912d9;hb=78229b5b53f947df657547e682c5365bbba9455b;hp=1f49c1ac5883feedc608b162bf6e02adb445288e;hpb=4f04bf7d4032d301ce723fce357a27f92f003893;p=helm.git diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 1f49c1ac5..0086f6aea 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -139,8 +139,11 @@ let _ = addDebugItem "dump moo to stderr" (fun _ -> let status = (MatitaScript.current ())#status in let moo = status.moo_content_rev in - List.iter (fun cmd -> prerr_endline - (GrafiteAstPp.pp_cic_command cmd)) (List.rev moo)); + List.iter + (fun cmd -> + prerr_endline (GrafiteAstPp.pp_command ~obj_pp:(fun _ -> assert false) + cmd)) + (List.rev moo)); addDebugItem "print metasenv goals and stack to stderr" (fun _ -> prerr_endline ("metasenv goals: " ^ String.concat " "