package coq
type state = Proofview_monad.Logical.Unsafe.stateval repr : 'a tactic -> ('a, state, state, Util.iexn) Logic_monad.BackState.tval make : ('a, state, state, Util.iexn) Logic_monad.BackState.t -> 'a tactictype state = Proofview_monad.Logical.Unsafe.stateval repr : 'a tactic -> ('a, state, state, Util.iexn) Logic_monad.BackState.tval make : ('a, state, state, Util.iexn) Logic_monad.BackState.t -> 'a tactic