Module Core.Tactic

module S := CodeUnit.Syntax
module D := CodeUnit.Domain
module RM := RefineMonad
module type Tactic = sig ... end
module Tp : sig ... end
module Chk : sig ... end
module Syn : sig ... end
module Tele : sig ... end
module KanTele : sig ... end
module Var : sig ... end
type var = Var.tac
val abstract : ?ident:Ident.t -> D.tp -> (var -> 'a RM.m) -> 'a RM.m
val abstract_tele : D.tele -> (var list -> 'a RM.m) -> 'a RM.m
val abstract_kan_tele : D.kan_tele -> (var list -> 'a RM.m) -> 'a RM.m