- let xmldump_observer _ (status, _) = print_endline proof#toString in
- ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- xmldump_observer);
-(*
- let proof_observer _ (status, ()) =
-prerr_endline "proof_observer";
- let ((uri_opt, metasenv, bo, ty), _) = status in
+ let xmldump_observer _ _ = print_endline proof#toString in
+ let proof_observer _ (status, metadata) =
+ debug_print "proof_observer";
+ let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
+ ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
+ metadata
+ in
+ let ((uri_opt, _, _, _), _) = status in