Forked from
Iris / Iris
Source project has a limited visibility.
-
Tej Chajed authored
Merge the "1 focused goal" line with the subsequent "(shelved: 1)" line, since this is the new output in Coq 8.15+. Iris does not currently produce this output, since no test calls `Show` with shelved goals, but this future-proofs the test normalization.
Tej Chajed authoredMerge the "1 focused goal" line with the subsequent "(shelved: 1)" line, since this is the new output in Coq 8.15+. Iris does not currently produce this output, since no test calls `Show` with shelved goals, but this future-proofs the test normalization.