type tactic
val goal_of_conjecture: conjecture -> goal
- val is_goal_in_metasenv: metasenv -> goal -> bool
+ val goal_mem: goal -> metasenv -> bool
val apply_tactic:
tactic -> metasenv -> goal ->
type t =
| Dot
| Semicolon
+
| Branch
| Shift of int option
| Merge
+
| Select of E.goal list
| End_select
+
| Tactical of tactical
+ | Qed
+
val eval: t -> status -> status
+ val init: E.metasenv -> status
end