Issues · Iris / Iris · GitLab

Remove duplicate abstraction

#218 · opened Oct 26, 2018 by Ghost User
- CLOSED
- 1
updated Oct 29, 2018
Explore getting rid of implication

#215 · opened Oct 13, 2018 by Ralf Jung A-theory
- CLOSED
- 8
updated Nov 01, 2019
Werid bug with `env_notations` and stdpp's `destruct_and!` tactic.

#214 · opened Oct 11, 2018 by Dan Frumin
- CLOSED
- 4
updated Oct 12, 2018
Moving hypotheses from the intuitionistic to the spatial context

#213 · opened Oct 04, 2018 by Robbert A-coq C-enhancement T-proofmode
- CLOSED
- 1
- 0
updated Feb 18, 2020
Masks are coPsets in the Coq development, not arbitrary subsets of natural numbers

#211 · opened Oct 01, 2018 by Joseph Tassarotti A-docs C-enhancement
- CLOSED
- 1
- 1
updated Mar 18, 2020
Iris 3.1.0 is compatible with Coq 8.8.1 and coq-mathcomp-ssreflect 1.7.0

#209 · opened Aug 29, 2018 by Janno
- CLOSED
- 2
updated Aug 29, 2018
Import Coq.Strings.Ascii before using ascii notations

#208 · opened Aug 24, 2018 by Ghost User
- CLOSED
- 10
updated Aug 24, 2018
Rule "Res-Alloc" in documentation is stronger than the Coq version

#207 · opened Aug 16, 2018 by Joseph Tassarotti
- CLOSED
- 1
- 6
updated Mar 06, 2019
Missing error message with `iDestruct ... as "#..."`

#206 · opened Jul 31, 2018 by Ralf Jung T-proofmode
- CLOSED
- 1
- 4
updated Jan 23, 2019
Support `iInduction .. using ...`

#204 · opened Jul 10, 2018 by Robbert
- CLOSED
- 0
updated Aug 29, 2018
Improve "... not found" error messages

#201 · opened Jun 14, 2018 by Ralf Jung T-proofmode
- CLOSED
- 1
updated Jan 11, 2019
Framing: Make* classes lead to suboptimal results

#200 · opened Jun 13, 2018 by Ralf Jung T-proofmode
- CLOSED
- 2
updated Jul 13, 2018
iSplitL no longer checks if assumptions are spatial

#199 · opened Jun 10, 2018 by Ralf Jung T-proofmode
- CLOSED
- 3
updated Jun 10, 2018
iAlways fails without a proper error message

#198 · opened Jun 10, 2018 by Ralf Jung T-proofmode
- CLOSED
- 1
- 1
updated Jul 13, 2018
iFrame sometimes needs to be called twice

#197 · opened Jun 10, 2018 by Ralf Jung T-proofmode
- CLOSED
- 21
updated Jun 14, 2018
coq-speed: Measure using performance counters

#194 · opened Jun 05, 2018 by Ralf Jung A-infra
- CLOSED
- 15
updated Jun 22, 2018
Remove or fix `base_logic/deprecated.v`

#193 · opened Jun 05, 2018 by Robbert Generalized Proofmode Merger T-proofmode
- CLOSED
- 1
- 3
updated Jul 13, 2018
Document `iRewrite -...` in `ProofMode.md`

#192 · opened Jun 04, 2018 by Dan Frumin
- CLOSED
- 3
updated Jan 11, 2019
Printing of the sequence operator `;;`

#191 · opened Jun 04, 2018 by Marianna Rapoport
- CLOSED
- 3
updated Jun 13, 2018
Framing persistent hypotheses under a later in the goal

#190 · opened May 31, 2018 by Hai Dang
- CLOSED
- 1
- 1
updated Jul 13, 2018

Prev
1
2
3
4
5
6
7
8
…
12
Next