Do not call `done` recursively when solving `is_Some`. (!296) · Merge requests · Iris / stdpp

Merged Robbert Krebbers requested to merge robbert/done_is_Some_non_rec into master 3 years ago

Status	Pipeline	Stages
Passed 00:04:39 3 years ago	Apply 1 suggestion(s) to 1 file(s) #50451 296 53a108a6	Stage: build	Download artifacts No artifacts found
Passed 00:05:02 3 years ago	Use `fast_done` as suggested by @jung. #50432 296 967cda05	Stage: build	Download artifacts No artifacts found
Passed 00:05:01 3 years ago	Test. #50431 296 fe9fe32a	Stage: build	Download artifacts No artifacts found

Do not call `done` recursively when solving `is_Some`.