Skip to content

GitLab

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

Switch branch/tag
  • iris
  • theories
  • proofmode
  • class_instances.v
Find file BlameHistoryPermalink
  • Robbert Krebbers's avatar
    Make IntoLaterN work on ▷ ?P with ?P an evar. · 1e241cca
    Robbert Krebbers authored Mar 10, 2017
    Also, make the setup of IntoLaterN more consistent with that of WandWeaken.
    Maybe, we should do something similar for other proof mode classes too.
    1e241cca

Replace class_instances.v

Attach a file by drag & drop or click to upload


Cancel
GitLab will create a branch in your fork and start a merge request.