- (* TODO Zack a lot:
- * - ids_to_inner_types, ids_to_inner_sorts handling
- * - sequent viewer notification
- *)
- 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, (proof_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) =
+ proof_metadata
+ in
+ let ((uri_opt, _, _, _), _) = status in