Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 122
    • Issues 122
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 18
    • Merge Requests 18
  • 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
  • Iris
  • Issues

  • Open 122
  • Closed 263
  • All 385
New issue
  • Priority Created date Last updated Milestone due date Due date Popularity Label priority Manual
  • Proof mode only *mostly* works when it is transitively imported, not exported
    #111 · opened Nov 16, 2017 by Ralf Jung   Iris 3.1   T-proofmode
    • CLOSED
    • 7
    updated Nov 20, 2017
  • iIntros on pure implications stopped working
    #108 · opened Oct 28, 2017 by Ralf Jung   Iris 3.1   T-proofmode
    • CLOSED
    • 7
    updated Oct 28, 2017
  • Reverting to old (stronger) definition of atomicity
    #107 · opened Oct 27, 2017 by Amin Timany   Iris 3.1
    • CLOSED
    • 1
    • 17
    updated Oct 29, 2017
  • Iris 3.1   3 of 4 tasks completed
    #106 · opened Oct 27, 2017 by Ralf Jung   Iris 3.1
    • CLOSED
    • 8
    updated Jan 09, 2018
  • Add some theory about the interaction of plainly and fancy updates
    #105 · opened Oct 27, 2017 by Ralf Jung   Iris 3.1
    • CLOSED
    • 1
    • 2
    updated Nov 01, 2017
  • Proof mode notation broken depending on import order
    #100 · opened Sep 29, 2017 by Ralf Jung   Iris 3.1   T-proofmode
    • CLOSED
    • 15
    updated Nov 11, 2017
  • Let iAlways clear the spatial context
    #81 · opened Mar 16, 2017 by Ralf Jung   Iris 3.1   T-proofmode
    • CLOSED
    • 16
    updated Oct 27, 2017
  • Stronger Invariant Allocation Rules
    #59 · opened Dec 29, 2016 by Janno   Iris 3.0
    • CLOSED
    • 9
    updated Jan 11, 2017
  • iAssert ... as %X should get all assumptions
    #56 · opened Dec 20, 2016 by Ralf Jung   Iris 3.0   T-proofmode
    • CLOSED
    • 1
    updated Jan 03, 2017
  • iNext unfolds things (more than simpl) even when there is no later to strip
    #55 · opened Dec 20, 2016 by Ralf Jung   Iris 3.0   T-proofmode
    • CLOSED
    • 10
    updated Feb 20, 2018
  • iIntros fails to introduce Coq-level and Iris-level universal quantifiers at once
    #54 · opened Dec 19, 2016 by Ralf Jung   Iris 3.0   T-proofmode
    • CLOSED
    • 3
    updated Dec 21, 2016
  • iMod and evar instantiation
    #52 · opened Dec 19, 2016 by Ralf Jung   Iris 3.0   T-proofmode
    • CLOSED
    • 4
    updated Jun 17, 2019
  • `contains` is named the wrong way around
    #50 · opened Dec 14, 2016 by Ralf Jung   Iris 3.0
    • CLOSED
    • 42
    updated Jan 14, 2017
  • Use opam-based CI
    #47 · opened Nov 30, 2016 by Ralf Jung   Iris 3.0
    • CLOSED
    • 2
    updated Dec 14, 2016
  • Renaming things
    #35 · opened Sep 29, 2016 by Ralf Jung   Iris 3.0
    • CLOSED
    • 42
    updated Nov 09, 2016
  • wp_bind does not report a failure message
    #401 · opened Feb 02, 2021 by Tej Chajed
    • CLOSED
    • 1
    • 0
    updated Feb 02, 2021
  • fupd_plainly_laterN = fupd_plain_laterN ?
    #393 · opened Dec 23, 2020 by Paolo G. Giarrusso
    • CLOSED
    • 1
    • 1
    updated Dec 23, 2020
  • Dropping support for Coq 8.10
    #388 · opened Dec 04, 2020 by Tej Chajed   A-coq
    • CLOSED
    • 1
    • 1
    • 2
    updated Dec 16, 2020
  • Deprecate unqualified "Instance"
    #387 · opened Dec 03, 2020 by Ralf Jung   A-coq C-enhancement T-style
    • CLOSED
    • 4
    updated Dec 19, 2020
  • Quote does not handle ⊣⊢
    #373 · opened Nov 03, 2020 by Rodolphe Lepigre
    • CLOSED
    • 1
    updated Nov 05, 2020
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • 6
  • …
  • 14
  • Next