Signature (cooltt.Core.Refiner.Signature)

val formation : Tactic.Tele.tac -> Tactic.Tp.tac

val intro : 
  [ `Field of Ident.t * Tactic.Chk.tac
  | `Include of Tactic.Syn.tac * (Ident.t -> Ident.t option) ]
    list ->
  Tactic.Chk.tac

val proj : Tactic.Syn.tac -> Ident.t -> Tactic.Syn.tac