Skip to content
GitLab

Add a `NoBackTrack` type class.

Merged Robbert Krebbers requested to merge robbert/NoBackTrack into master

NoBackTrack P requires P but will never backtrack on it once a result for P has been found.

See also https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112