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 62
    • Issues 62
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 2
    • Merge requests 2
  • 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
  • !365

Closed
Created Jan 20, 2022 by Matthieu Sozeau@mattam82Contributor
  • Report abuse
Report abuse

Draft: Overlay for PR#15518

  • Overview 14
  • Commits 1
  • Pipelines 2
  • Changes 4

This is an overlay for Coq PR #15518: moving apply to the evar-based unifier. This includes a breaking fix for apply of conjunction which has the unnatural behavior of trying Q -> P before P -> Q when applying a P <-> Q hypothesis. I think the rest is backwards compatible: mostly about using eapply in places where new existential are created, which the new apply forbids (rightfully).

Edited May 06, 2022 by Ralf Jung
Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: coq-pr-15518