Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Group overview
    • Group overview
    • Details
    • Activity
  • Issues 196
    • Issues 196
    • List
    • Board
    • Labels
    • Milestones
  • Merge Requests 26
    • Merge Requests 26
  • Packages & Registries
    • Packages & Registries
    • Package Registry
    • Dependency Proxy
  • Members
    • Members
Collapse sidebar
  • Iris
  • Issues

  • Open 196
  • Closed 341
  • All 537
  • Priority Created date Last updated Milestone due date Due date Popularity Label priority Manual
  • `iRename` fails with bad error message when not in proof mode
    iris#397 · opened Jan 12, 2021 by Robbert
    • 1
    updated Jan 12, 2021
  • Intro pattern `>` has wrong behavior with side-conditions of `iMod`
    iris#396 · opened Jan 12, 2021 by Robbert
    • 3
    updated Jan 12, 2021
  • "pred" is printed strangely
    stdpp#92 · opened Jan 11, 2021 by Ralf Jung
    • 0
    updated Jan 11, 2021
  • Use Iris' library for partial bijections
    reloc#9 · opened Jan 11, 2021 by Dan Frumin
    • 0
    updated Jan 11, 2021
  • Generalize frac to dfrac in view camera
    iris#395 · opened Jan 04, 2021 by Simon Friis Vindum   A-coq C-enhancement T-algebra
    • 1
    • 2
    updated Jan 16, 2021
  • Document relation between Discrete and Timeless (in appendix?)
    iris#394 · opened Dec 23, 2020 by Paolo G. Giarrusso   A-docs T-algebra T-base_logic
    • 0
    updated Jan 06, 2021
  • Masks in step-taking fupd notation
    iris#392 · opened Dec 10, 2020 by Ralf Jung   A-theory C-enhancement T-base_logic
    • 1
    • 0
    updated Dec 10, 2020
  • What generation condition for types?
    refinedc#31 · opened Dec 09, 2020 by Rodolphe Lepigre   frontend usability
    • 0
    updated Dec 09, 2020
  • Paper cuts   3 of 8 tasks completed
    refinedc#30 · opened Dec 09, 2020 by Michael Sammler   frontend usability
    • 1
    updated Dec 15, 2020
  • Add append-only list RA to Iris
    iris#391 · opened Dec 08, 2020 by Ralf Jung   A-coq C-enhancement T-algebra T-base_logic
    • 0
    updated Dec 09, 2020
  • Citation guide
    iris#389 · opened Dec 06, 2020 by Tej Chajed   A-docs
    • 1
    updated Dec 08, 2020
  • No `ident_to_string`?
    string-ident#5 · opened Dec 04, 2020 by Joachim Breitner
    • 1
    updated Dec 04, 2020
  • reshape_expr does not recognize `fill`
    iris#385 · opened Nov 27, 2020 by Ralf Jung   A-coq C-enhancement T-heap_lang
    • 0
    updated Dec 05, 2020
  • Better typing error messages   0 of 2 tasks completed
    refinedc#26 · opened Nov 23, 2020 by Michael Sammler   feature usability
    • 0
    updated Nov 23, 2020
  • Make sure we have Hint Mode for every typeclass   0 of 1 task completed
    iris#381 · opened Nov 12, 2020 by Ralf Jung   A-coq C-bug T-style
    • 0
    updated Nov 12, 2020
  • iDestruct does not handle some patterns that it probably could
    iris#380 · opened Nov 11, 2020 by Tej Chajed   A-coq C-enhancement T-proofmode
    • 1
    • 0
    updated Nov 11, 2020
  • Make sealing consistent and document it
    iris#379 · opened Nov 10, 2020 by Ralf Jung   A-coq A-docs C-enhancement T-style
    • 0
    updated Nov 10, 2020
  • Graveyard for obsolete code
    iris#378 · opened Nov 10, 2020 by Robbert   A-coq
    • 3
    updated Dec 07, 2020
  • We have some lonely notations
    iris#375 · opened Nov 05, 2020 by Ralf Jung   A-coq C-bug T-style
    • 0
    updated Nov 05, 2020
  • Avoid sequences of "_" by adjusting lemma statements
    iris#374 · opened Nov 05, 2020 by Ralf Jung   A-coq C-enhancement T-style
    • 0
    updated Nov 05, 2020
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • …
  • 10
  • Next