Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 61
    • Issues 61
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 5
    • Merge requests 5
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !212

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

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge ci/robbert/seq_S into master Jan 11, 2021
  • Overview 2
  • Commits 2
  • Pipelines 3
  • Changes 2

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.

Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: ci/robbert/seq_S