added contextual menu to act over selected terms

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 1f49c1ac5883feedc608b162bf6e02adb445288e..0086f6aeac3f5a48860d13f358837191ee4912d9 100644 (file)
--- 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 " "