Skip to content

Let `done` and friends fail when the proofmode goal is an evar.

Robbert Krebbers requested to merge robbert/done_evar into gen_proofmode

This fixes issue #182 (closed) and is an alternative for !139 (closed).

See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/139#note_26680 for my motivation.

Merge request reports