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
  • Adding rules for intptr casts.
    refinedc!10 · opened Dec 07, 2020 by Rodolphe Lepigre
    • MERGED
    • 3
    updated Dec 09, 2020
  • Add missing `Hint Mode` for `ghost_var` and `gset_bij`; fix arguments of `gset_bijG`
    iris!601 · opened Dec 07, 2020 by Robbert
    • MERGED
    • 1
    updated Dec 07, 2020
  • mono_nat_update: make first argument implicit
    iris!600 · opened Dec 07, 2020 by Ralf Jung
    • MERGED
    • 1
    updated Dec 07, 2020
  • Add support for macros
    refinedc!7 · opened Dec 02, 2020 by Michael Sammler
    • MERGED
    • 6
    updated Dec 07, 2020
  • Rename `mnat`/`mnat_auth` into `mono_nat`.
    iris!572 · opened Nov 05, 2020 by Robbert   Iris 3.4
    • MERGED
    • 40
    updated Dec 06, 2020
  • Remove `CopyDestruct` heuristic
    iris!596 · opened Dec 02, 2020 by Robbert   Iris 3.4
    • MERGED
    • 19
    updated Dec 06, 2020
  • Use user-supplied names when destructing existentials with ? intro pattern
    iris!479 · opened Jul 18, 2020 by Tej Chajed
    • MERGED
    • 64
    updated Dec 05, 2020
  • wp_finish: avoid making a goal unprovable
    iris!593 · opened Nov 26, 2020 by Ralf Jung
    • MERGED
    • 25
    updated Dec 05, 2020
  • add gmap_view_alloc_big
    iris!598 · opened Dec 04, 2020 by Ralf Jung
    • MERGED
    • 5
    updated Dec 04, 2020
  • Make iDestruct consume wands when it's supposed to
    iris!591 · opened Nov 25, 2020 by Tej Chajed   T-proofmode
    • MERGED
    • 16
    updated Dec 04, 2020
  • add insert_subseteq_l
    stdpp!204 · opened Dec 04, 2020 by Ralf Jung
    • MERGED
    • 3
    updated Dec 04, 2020
  • Upgrade README demo: it_max -> max_int.
    refinedc!9 · opened Dec 04, 2020 by Fengmin Zhu
    • MERGED
    • 1
    updated Dec 04, 2020
  • Intptr
    refinedc!8 · opened Dec 04, 2020 by Michael Sammler
    • MERGED
    • 0
    updated Dec 04, 2020
  • Add explicit Local/Global to hints at top level
    iris!594 · opened Nov 27, 2020 by Tej Chajed
    • MERGED
    • 13
    updated Dec 03, 2020
  • Add explicit Global to hints at top level
    stdpp!202 · opened Nov 20, 2020 by Tej Chajed
    • MERGED
    • 5
    updated Dec 03, 2020
  • link to pinned-package-versions page
    iris!590 · opened Nov 23, 2020 by Ralf Jung
    • MERGED
    • 1
    updated Dec 03, 2020
  • Protocol equivalence
    actris!24 · opened Nov 25, 2020 by Jonas Kastberg
    • MERGED
    • 0
    updated Dec 02, 2020
  • Use separate inductives for allocation (refactoring).
    refinedc!6 · opened Dec 02, 2020 by Rodolphe Lepigre
    • MERGED
    • 11
    updated Dec 02, 2020
  • make pure_exec_fill not an instance any more
    iris!588 · opened Nov 13, 2020 by Ralf Jung
    • MERGED
    • 16
    updated Nov 29, 2020
  • Add a good failure state for allocation failure   6 of 6 tasks completed
    refinedc!5 · opened Nov 26, 2020 by Rodolphe Lepigre
    • MERGED
    • Approved
    • 0
    updated Nov 27, 2020
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • 6
  • 7
  • …
  • 42
  • Next