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 4
    • Merge requests 4
  • 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
  • !375

Annotate telescope notations to support literal telescope arguments.

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Janno requested to merge janno/fix-TargS-notation into master May 03, 2022
  • Overview 12
  • Commits 2
  • Pipelines 2
  • Changes 2

!368 (merged) had the unfortunate consequence that literal telescope arguments would not typecheck any more. This MR fixes this by adding copious (but nonetheless minimal) amounts of casts and annotations to make the [tele_arg ..] notation work again. I added tests for both new and old unification.

I am currently running a full test with these changes on all BedRock proofs which should tell us a bit about the compatibility. I expect no problems here.

Something that is not reflected in the MR but is still interesting is that old unification, i.e. apply and friends, work even without the cast in the TargS notation. New unification, i.e. refine, does not. There might be a Coq bug to report here but I don't have time to dig into that right now.

Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: janno/fix-TargS-notation