sig
type kind =
K_Assert
| K_Invariant
| K_Variant
| K_StmtSpec
| K_Allocation
| K_Assigns
| K_Decreases
| K_Terminates
| K_Complete
| K_Disjoint
| K_Requires
| K_Ensures
val clear : unit -> unit
val push : Kernel_function.t -> Keep_status.kind -> Property.t -> unit
val before_translation : unit -> unit
val must_translate : Kernel_function.t -> Keep_status.kind -> bool
end