module ApplyResult:sig
..end
ApplyResult objects represent the result of an application of a
tactic to a goal. It contains the subgoals that were produced.
type
apply_result
val get_num_subgoals : apply_result -> int
val get_subgoals : apply_result -> Goal.goal list
val get_subgoal : apply_result -> int -> Goal.goal
val convert_model : apply_result -> int -> Model.model -> Model.model
g
, that the ApplyResult was obtained from.
#return A model for g
val to_string : apply_result -> string