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
  • iDestruct and iPureIntro
    #21 · opened Jul 27, 2016 by Ghost User   A-coq C-enhancement T-proofmode
    • CLOSED
    • 3
    updated Nov 01, 2019
  • Ticket lock proof
    #22 · opened Aug 01, 2016 by Ghost User
    • CLOSED
    • 0
    updated Aug 02, 2016
  • iFrame should support conjunction
    #23 · opened Aug 02, 2016 by Ghost User
    • CLOSED
    • 8
    updated Aug 02, 2016
  • Find nice syntax for our "CPS" WP specifications
    #24 · opened Aug 05, 2016 by Ralf Jung
    • CLOSED
    • 2
    updated Oct 27, 2016
  • iSplitL "persistent_hyp": Improve error
    #25 · opened Aug 05, 2016 by Ralf Jung   T-proofmode
    • CLOSED
    • 0
    updated Aug 06, 2016
  • heap-lang CAS capability
    #26 · opened Aug 08, 2016 by Ghost User
    • CLOSED
    • 14
    updated Oct 21, 2016
  • mathpartir.sty is missing
    #27 · opened Aug 09, 2016 by Jeehoon Kang
    • CLOSED
    • 3
    updated Aug 09, 2016
  • docs: the universe $\cal U$ is used without definition
    #28 · opened Aug 14, 2016 by Jeehoon Kang
    • CLOSED
    • 0
    updated Aug 16, 2016
  • Bring back Logically Atomic Triples (Coq + docs)   1 of 2 tasks completed
    #29 · opened Aug 16, 2016 by Jeehoon Kang   A-theory C-project T-logical-atomicity
    • 7
    updated Nov 01, 2019
  • Make coqchk (make verify) work
    #30 · opened Aug 19, 2016 by Ralf Jung
    • CLOSED
    • 5
    updated Aug 19, 2016
  • iMod doesn't handle mismatched mask
    #31 · opened Aug 23, 2016 by Ghost User   A-coq C-enhancement T-proofmode
    • 1
    • 20
    updated Oct 02, 2020
  • Support framing pure/Coq hypotheses
    #32 · opened Sep 05, 2016 by Jacques-Henri Jourdan
    • CLOSED
    • 5
    updated Sep 19, 2016
  • Confusing error msg for `iTimeless`
    #33 · opened Sep 12, 2016 by Ghost User   T-proofmode
    • CLOSED
    • 10
    updated Oct 27, 2016
  • Coq induction support in proof mode
    #34 · opened Sep 12, 2016 by Jacques-Henri Jourdan
    • CLOSED
    • 7
    updated Sep 30, 2016
  • Renaming things
    #35 · opened Sep 29, 2016 by Ralf Jung   Iris 3.0
    • CLOSED
    • 42
    updated Nov 09, 2016
  • STSs: Consider changing the def. of frame-steps
    #36 · opened Sep 29, 2016 by Ralf Jung   A-theory C-project T-algebra
    • CLOSED
    • 5
    updated Nov 01, 2019
  • saved_prop for predicate
    #37 · opened Oct 05, 2016 by Ghost User
    • CLOSED
    • 8
    updated Oct 05, 2016
  • Refactor bigops
    #38 · opened Oct 10, 2016 by Ralf Jung
    • CLOSED
    • 1
    • 4
    updated Apr 01, 2017
  • iIntros: bad error when trying to use a name that's already used
    #39 · opened Oct 26, 2016 by Ralf Jung   T-proofmode
    • CLOSED
    • 1
    updated Oct 26, 2016
  • iRewrite and internal equality on predicates
    #40 · opened Oct 27, 2016 by Janno
    • CLOSED
    • 4
    updated Oct 27, 2016
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • 6
  • …
  • 20
  • Next