Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
L
lambda-rust
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 3
    • Issues 3
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 0
    • Merge Requests 0
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Iris
  • lambda-rust
  • Merge Requests
  • !3

Merged
Opened Dec 01, 2016 by Ralf Jung@jungOwner

Coq 8.6

  • Overview 6
  • Commits 2
  • Changes 4

These are the changes necessary to make this compatible with Coq 8.6. Most of the changes are fine (and of the category "no idea why this worked in 8.5" or "the statement of a lemma changed in the 8.6 libs"), except for the horribleness in perm_incl.v. I played around a little but found no good way to restore the term into the state Coq 8.5 put it in -- and the goals I end up in otherwise (if I just remove the change) look fairly unsolvable.

Cc @jjourdan @robbertkrebbers

Assignee
Assign to
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/lambda-rust!3
Source branch: coq-8.6

Revert this merge request

This will create a new commit in order to revert the existing changes.

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.

Cherry-pick this merge request

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.