Skip to content
Snippets Groups Projects

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

Merged 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
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
Please register or sign in to reply
Loading