Skip to content

Rename `seq_S_snoc` into `seq_S` to be consistent with Coq's stdlib

Robbert Krebbers requested to merge ci/robbert/seq_S into master

The lemma seq_S is present in Coq's stdlib since Coq 8.12, and is the same as our lemma seq_S_snoc.

MR !211 (merged) accidentally used the lemma seq_S from the stdlib, and hence CI failed with Coq 8.10 and Coq 8.11.

This MR adds a copy of the lemma from the stdlib, which we can remove once we drop support for Coq 8.10 and Coq 8.11.

Merge request reports

Loading