(** [target_exists [t1; t2; ...]] is the same as writing
[target (t1 || t2 || ...)] *)
-val require : (unit -> unit) -> unit
+val require : string -> (unit -> unit) -> unit
(** [require] {i goal} defines the requirements of this goal, that
is, other goals that have to be met before the rest of the
goal is able to run.
(* Export this so the macros can catch these exceptions. *)
type goal_result_t = Goal_OK | Goal_failed of string
exception Goal_result of goal_result_t
+
+(* Called to print debug message when we enter or leave a goal. *)
+val _enter_goal : string -> unit
+val _leave_goal : string -> unit