This modules reifies Coq side effects into an algebraic structure.

Must be hooked to allow Protect to capture the feedback.

Eval a function and reify the exceptions. Note f _must_ be pure, as in case of anomaly f may be re-executed with debug options. Beware, not thread-safe!