Support constructor closures

[Lysxia]

Close #2223

Generate a simplified body of the closure (directly call the continuation after asserting the expected invariant):

let c_Some [@coma:extspec] (x: a) (return (x: option_a) = {inv (Some x)} return {Some x}

Then reuse the pre- and post-conditions inferred by Coma (c_Some'pre, c_Some'post'return).

[jhjourdan]

Out of curiosity, why did you not choose to synthesize the pre- and postconditions?

[Lysxia]

Looking for an excuse to use coma:extspec.