metadata are no longer stored in .moo files.

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 0a83b737ebe54e7ee4dd7db23c9bd1eb824bd0e1..769f294fd2ef6d2743ef4d925bee4c3191afb3c2 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -139,11 +139,9 @@ let _ =
       CicNotationParser.print_l2_pattern;
     addDebugItem "dump moo to stderr" (fun _ ->
       let status = (MatitaScript.current ())#status in
-      let moo, metadata = status.moo_content_rev 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 m -> prerr_endline
-        (GrafiteAstPp.pp_metadata m)) metadata);
+        (GrafiteAstPp.pp_cic_command cmd)) (List.rev moo));
     addDebugItem "print metasenv goals and stack to stderr"
       (fun _ ->
         prerr_endline ("metasenv goals: " ^ String.concat " "