Attribute Macro coq_after

Source
#[coq_after]