+let require name f =
+ indent "require: %s\n" name;
+ incr depth;
+ let r = (try Either (f ()) with exn -> Or exn) in
+ decr depth;
+ match r with
+ | Either x -> x
+ | Or exn -> raise exn
+
+let _enter_goal name = indent "enter goal: %s\n" name
+let _leave_goal name = indent "leave goal: %s\n" name