Allow catching of EvaluatedError exceptions.

We export `Cerrors.EvaluatedError` so plugins and STM consumers can
catch it.

It took me a while to make my mind on this one, but now I am convinced
this is the right thing to do. (Another possibility is to remove
`EvaluatedError` altogether).

The rationale is as follows: when using `Stm.{add,observe}` it
will be frequent for Coq to raise a public-facing exception, however the
toplevel will wrap it into the `EvaluatedError`.

Thus, we get exceptions that we are supposed to handle, but its wrapping
in `EvaluatedError` prevents us from a more meaningful exception
handling: we are stuck with calling the printer.

In particular, this allows SerAPI/jsCoq to provide proper serialization
of most public exceptions.

0 files changed, 0 insertions, 0 deletions