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 29
    • Merge Requests 29
  • Packages & Registries
    • Packages & Registries
    • Package Registry
    • Dependency Proxy
  • Members
    • Members
Collapse sidebar
  • Iris
  • Merge Requests

  • Open 29
  • Merged 839
  • Closed 104
  • All 972
  • Priority Created date Last updated Milestone due date Popularity Label priority
  • Add `head_prim_fill_reducible`.
    iris!293 · opened Jul 12, 2019 by Dan Frumin   Iris 3.2
    • MERGED
    • 4
    updated Nov 24, 2020
  • Add simplification instance for list ≠ [], needed for quicksort
    refinedc!4 · opened Nov 24, 2020 by Ike Mulder
    • MERGED
    • 3
    updated Nov 24, 2020
  • move algebra.base -> prelude.prelude
    iris!586 · opened Nov 12, 2020 by Ralf Jung
    • MERGED
    • 9
    updated Nov 12, 2020
  • adding allocation range ghost state.
    refinedc!3 · opened Nov 05, 2020 by Rodolphe Lepigre
    • MERGED
    • 0
    updated Nov 12, 2020
  • Set `Hint Mode` for `pretty`.
    stdpp!201 · opened Nov 12, 2020 by Robbert
    • MERGED
    • 2
    updated Nov 12, 2020
  • Add back a proofmode test for issue #288
    iris!584 · opened Nov 11, 2020 by Tej Chajed
    • MERGED
    • 1
    updated Nov 11, 2020
  • Use original pattern in iDestruct error messages
    iris!550 · opened Oct 20, 2020 by Tej Chajed   S-waiting-for-review
    • MERGED
    • 28
    updated Nov 11, 2020
  • Pretty-print 0 as "0" for N, Z, and nat
    stdpp!200 · opened Nov 09, 2020 by Robbert
    • MERGED
    • 3
    updated Nov 11, 2020
  • multi-package repositories
    iris!514 · opened Sep 26, 2020 by Ralf Jung   S-waiting-for-review
    • MERGED
    • 1
    • 31
    updated Nov 11, 2020
  • add big_opM_singletons
    iris!567 · opened Nov 04, 2020 by Ralf Jung
    • MERGED
    • 10
    updated Nov 11, 2020
  • avoid (e)apply in wp_expr_eval
    iris!582 · opened Nov 11, 2020 by Ralf Jung
    • MERGED
    • 2
    updated Nov 11, 2020
  • wp_pures: also handle [WP v]
    iris!578 · opened Nov 09, 2020 by Ralf Jung
    • MERGED
    • 5
    updated Nov 11, 2020
  • Rename mapsto_mapsto_ne and add easier-to-use variant
    iris!574 · opened Nov 05, 2020 by Ralf Jung
    • MERGED
    • 8
    updated Nov 10, 2020
  • Make bulleting strict for algebra and base_logic
    iris!563 · opened Nov 03, 2020 by Tej Chajed
    • MERGED
    • 22
    updated Nov 10, 2020
  • provide _big variant of gen_heap_init
    iris!580 · opened Nov 10, 2020 by Ralf Jung
    • MERGED
    • 15
    updated Nov 10, 2020
  • Documentation on Iris equalities (take 2)
    iris!575 · opened Nov 06, 2020 by Ralf Jung
    • MERGED
    • 14
    updated Nov 10, 2020
  • split RA docs into separate file, and general doc updates
    iris!576 · opened Nov 06, 2020 by Ralf Jung
    • MERGED
    • 7
    updated Nov 10, 2020
  • Seal ghost_var and mnat_own
    iris!571 · opened Nov 05, 2020 by Ralf Jung
    • MERGED
    • 5
    updated Nov 10, 2020
  • fix wp_bind with empty context
    iris!579 · opened Nov 09, 2020 by Ralf Jung
    • MERGED
    • 4
    updated Nov 10, 2020
  • Add lemmas about `list_to_map`
    stdpp!199 · opened Nov 09, 2020 by Simon Friis Vindum
    • MERGED
    • 6
    updated Nov 10, 2020
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • 6
  • 7
  • 8
  • 9
  • …
  • 42
  • Next