Osiris.Cut
val cut : Coq.def -> Coq.defs
cut def turns a single Coq toplevel definition into a nonempty list of such definitions. The marks CCut indicate where terms should be cut off.
cut def
CCut