Skip to content

Add a `NoBackTrack` type class.

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

Merge request reports