let mk_tactic f =
ProofEngineTypes.mk_tactic
(fun (proof, goal) as pstatus ->
- let stack = [ [ 1, Stack.Open goal ], [], [], Stack.NoTag ] in
+ let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
let istatus = pstatus, stack in
(* let ostatus = f istatus in
let ((proof, opened, _), _) = ostatus in *)