let intros = PrimitiveTactics.intros_tac () in
let subgoals = ProofEngineTypes.apply_tactic intros status in
(match subgoals with
let intros = PrimitiveTactics.intros_tac () in
let subgoals = ProofEngineTypes.apply_tactic intros status in
(match subgoals with