| Incomplete_proof ((proof, goal) as status) ->
sequents_viewer#load_sequents status;
sequents_viewer#goto_sequent goal
- | _ -> ()
+ | Proof proof ->
+ prerr_endline "sequents_viewer#load_logo_with_qed (no proof)"; ()
+ | No_proof ->
+ prerr_endline "sequents_viewer#load_logo (no proof)"; ()
+ | Intermediate _ ->
+ assert false (* only the engine may be in this state *)
in
script#addObserver sequents_observer;
script#addObserver browser_observer
let oc = open_out "env.dump" in
CicEnvironment.dump_to_channel oc;
close_out oc);
+ addDebugItem "load environment from \"env.dump\"" (fun _ ->
+ let ic = open_in "env.dump" in
+ CicEnvironment.restore_from_channel ic;
+ close_in ic);
+ addDebugItem "dump universes" (fun _ ->
+ List.iter (fun (u,_,g) ->
+ prerr_endline (UriManager.string_of_uri u);
+ CicUniv.print_ugraph g) (CicEnvironment.list_obj ())
+ );
addDebugItem "print selected terms" (fun () ->
let i = ref 0 in
List.iter