let print_proof_tree (root: proof_tree_node) =
  let print_pt_id n1 = print_int (Tree.get_node_label n1).pt_id;print_string " ; "
  in
  let print_pt_children_ids n1 = 
    print_string "Children of ";
    print_pt_id n1;print_string ": \n"; 
    print_string "["; 
    List.iter print_pt_id (Tree.get_children n1);
    print_string "]\n"
  in
  let print_pt_edge pt_e = 
    match pt_e with
        (op,i) ->  
          begin 
            print_string "op: ";
            Message.msg_printer Message.Debug Operation.print op ; 
            print_string "\n proof: " (* URGENT ! ;print_int i --TYPE ISSUES *)
          end
  in
  let print_pt_node_data n_data = 
    print_int n_data.pt_id;print_string "\n";
    Abstraction.print_proof_region n_data.pt_region;
    match n_data.covering_nodes with
        None -> print_string "Not covered \n"
      | Some(i,l) -> print_string "Covered \n"
  in

  let rec print_pt_node n =
    let _ = 
      match (Tree.get_parent_edge n) with
          None -> print_string "ROOT NODE Id: ";
        | Some(e) ->
            let par = Tree.get_source e in
              begin
                print_string "----par: ";print_pt_id par;print_string "\n";
                print_pt_edge (Tree.get_edge_label e);
                print_string "---->\n";
                print_string "INT NODE Id: "
              end 
    in
      print_pt_node_data (Tree.get_node_label n);
      print_pt_children_ids n;
      List.iter print_pt_node (Tree.get_children n)
  in
    print_pt_node root