* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let default_history_size = 20
exception No_goal_left
_data <- data
method set_goal goal =
+ _goal <- Some goal
+(*
let old_internal_status = self#internal_status in
_goal <- Some goal;
try
with (Data_failure _) as exn ->
self#set_internal_status old_internal_status;
raise exn
+*)
method uri = let (uri, _, _, _) = _proof in uri
method metasenv = let (_, metasenv, _, _) = _proof in metasenv