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 120
    • Issues 120
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 16
    • Merge Requests 16
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • Iris
  • Issues

  • Open 120
  • Closed 266
  • All 386
New issue
  • Priority Created date Last updated Milestone due date Due date Popularity Label priority Manual
  • Failure to find a proof of persistence
    #255 · opened Jul 19, 2019 by Dmitry Khalanskiy   A-coq C-bug S-blocked-by-coq T-algebra
    • CLOSED
    • 1
    • 12
    updated Mar 18, 2020
  • Reliance on `Export` bug
    #254 · opened Jul 09, 2019 by Maxime Dénès
    • CLOSED
    • 5
    updated Nov 01, 2019
  • Constructing CMRAs by giving isomorphism to CMRAs
    #253 · opened Jul 09, 2019 by Paolo G. Giarrusso   A-coq C-enhancement Good First Issue T-algebra
    • CLOSED
    • 1
    • 1
    • 5
    updated Nov 06, 2020
  • equivI lemma for sigT
    #250 · opened Jun 24, 2019 by Paolo G. Giarrusso
    • CLOSED
    • 1
    • 4
    updated Jun 25, 2019
  • Better solvers for properness/contractiveness
    #249 · opened Jun 21, 2019 by Paolo G. Giarrusso
    • CLOSED
    • 4
    updated Feb 13, 2020
  • Comparison with `=` and with CAS is not the same
    #248 · opened Jun 18, 2019 by Ralf Jung   T-heap_lang
    • CLOSED
    • 1
    • 25
    updated Jul 01, 2019
  • iInv does not behave as intended when the goal is an accessor
    #247 · opened Jun 18, 2019 by Ralf Jung
    • CLOSED
    • 1
    updated Nov 01, 2019
  • iEval (eauto) "corrupts" goal
    #246 · opened Jun 14, 2019 by Paolo G. Giarrusso
    • CLOSED
    • 1
    updated Jun 15, 2019
  • Add IntoAnd instance (and more) for array
    #245 · opened Jun 14, 2019 by Rodolphe Lepigre   Iris 3.2
    • CLOSED
    • 1
    updated Aug 13, 2019
  • Planning the Iris 3.2 release   0 of 1 task completed
    #242 · opened Jun 06, 2019 by Ralf Jung   Iris 3.2   A-meta C-enhancement
    • CLOSED
    • 1
    • 1
    • 3
    updated Nov 01, 2019
  • We have ambiguous coercion paths
    #240 · opened May 13, 2019 by Ralf Jung   A-coq C-bug T-algebra
    • CLOSED
    • 1
    • 7
    updated Apr 02, 2020
  • Iris logo
    #239 · opened May 06, 2019 by Robbert Krebbers   A-meta C-project
    • CLOSED
    • 27
    updated Feb 05, 2021
  • Wish: iSimpl on multiple hypothesis
    #238 · opened Apr 26, 2019 by Dan Frumin   C-enhancement T-proofmode
    • CLOSED
    • 1
    • 0
    updated May 22, 2019
  • Stripping laterN from pure propositions when proving laterN *without except-0*
    #237 · opened Apr 15, 2019 by Paolo G. Giarrusso
    • CLOSED
    • 2
    updated Nov 01, 2019
  • Non-expansiveness for big ops
    #236 · opened Apr 07, 2019 by Dan Frumin   A-coq C-enhancement Good First Issue T-bi
    • CLOSED
    • 4
    updated Mar 19, 2020
  • Syntactic type system for heap_lang   0 of 2 tasks completed
    #234 · opened Mar 29, 2019 by Robbert Krebbers   A-theory C-project T-heap_lang
    • CLOSED
    • 31
    updated Oct 01, 2020
  • Can't install on Coq 8.8.1
    #233 · opened Mar 19, 2019 by Maximilian Wuttke
    • CLOSED
    • 2
    updated Mar 20, 2019
  • Investigate slowdown caused by gset change
    #232 · opened Mar 14, 2019 by Ralf Jung
    • CLOSED
    • 1
    • 9
    updated Apr 24, 2019
  • Allow swapping later^i and forall, later, etc.
    #231 · opened Mar 02, 2019 by Paolo G. Giarrusso
    • CLOSED
    • 4
    updated Nov 01, 2019
  • "Generalizable All Variables" considered harmful
    #230 · opened Feb 22, 2019 by Ralf Jung
    • CLOSED
    • 4
    updated Feb 27, 2019
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • 6
  • 7
  • 8
  • …
  • 14
  • Next