Protect.Error
This modules reifies Coq side effects into an algebraic structure.
This is obviously very convenient for upper layer programming.
As of today this includes feedback and exceptions.
type 'l t = private
| User of 'l Message.Payload.t
| Anomaly of 'l Message.Payload.t