Skip to content
GitLab
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
  • Dmitry Khalanskiy
  • Iris
  • Repository
Switch branch/tag
  • iris
  • proofmode
  • coq_tactics.v
Find file BlameHistoryPermalink
  • Robbert Krebbers's avatar
    Also create a wand when reverting a persistent hypothesis. · 56301ac8
    Robbert Krebbers authored Oct 28, 2016
    This is more consistent with our current consensus of not using
    implication. Also, it allows one to reintroduce the persistent
    hypothesis into the spatial context.
    56301ac8