Issues · Iris / Iris

New issue

Break dependency of algebra on base_logic

#355 · created Oct 06, 2020 by Ralf Jung A-coq C-enhancement T-algebra T-base_logic
- CLOSED
- 1
- 0
updated Oct 20, 2020
CHANGELOG should spell out what changed in auth due to views MR better

#353 · created Oct 02, 2020 by Tej Chajed A-docs C-bug
- CLOSED
- 1
- 0
updated Oct 03, 2020
Typeclass inference fails to trigger.

#346 · created Sep 17, 2020 by Arthur Azevedo de Amorim A-coq C-support
- CLOSED
- 4
updated Sep 21, 2020
Check for `options.v` should only consider files in _CoqProject

#345 · created Sep 10, 2020 by Robbert Krebbers
- CLOSED
- 8
updated Sep 12, 2020
Set Default Goal Selector

#344 · created Sep 10, 2020 by Ralf Jung A-coq C-enhancement T-style
- CLOSED
- 1
- 3
updated Nov 10, 2020
Make CI fail when proofs depend on auto-generated names

#343 · created Sep 08, 2020 by Ralf Jung A-coq A-infra C-enhancement T-style
- CLOSED
- 2
- 2
updated Apr 12, 2021
Missing {u,}rFunctors and conversions

#342 · created Aug 20, 2020 by Paolo G. Giarrusso A-coq C-enhancement T-algebra
- CLOSED
- 1
- 1
updated Sep 10, 2020
Weird automatically generated names

#337 · created Jul 22, 2020 by Robbert Krebbers
- CLOSED
- 1
- 2
updated Aug 12, 2020
Use user-supplied names in iIntros (?)

#336 · created Jul 20, 2020 by Tej Chajed
- CLOSED
- 1
- 3
updated Aug 12, 2020
Iris Library Best Practices

#333 · created Jul 07, 2020 by Ralf Jung A-docs
- CLOSED
- 1
- 1
updated Aug 06, 2020
Add RA for auth of a heap

#328 · created Jun 23, 2020 by Ralf Jung A-coq C-enhancement T-algebra
- CLOSED
- 1
- 5
updated Oct 12, 2020
Add RA for auth max_nat

#327 · created Jun 19, 2020 by Robbert Krebbers A-coq C-enhancement T-algebra
- CLOSED
- 1
- 2
- 0
updated Oct 27, 2020
iSpecialize with "[% //]" does not report an error if done fails

#325 · created Jun 12, 2020 by Tej Chajed
- CLOSED
- 1
- 0
updated Jun 26, 2020
Add "nat+min" RA

#324 · created Jun 12, 2020 by Ralf Jung C-enhancement T-algebra
- CLOSED
- 1
- 9
updated Jun 18, 2020
Operator precedence in heap lang is wrong

#322 · created May 28, 2020 by Dmitry Khalanskiy
- CLOSED
- 4
updated May 28, 2020
Fix "omega is deprecated" warnings by switching to lia

#319 · created May 16, 2020 by Tej Chajed
- CLOSED
- 1
- 2
updated May 16, 2020
Drop support for Coq 8.9?

#318 · created May 12, 2020 by Ralf Jung A-coq
- CLOSED
- 1
- 2
updated Aug 24, 2020
Port HeapLang tactics to more efficient style

#315 · created Apr 29, 2020 by Robbert Krebbers A-coq C-enhancement I-performance T-heap_lang
- CLOSED
- 1
- 0
updated Jul 15, 2020
Argument to bi_pure should have argument at type_scope?

#314 · created Apr 26, 2020 by Gregory Malecha A-coq C-enhancement
- CLOSED
- 5
updated Jun 16, 2021
Add deallocation operation to HeapLang

#313 · created Apr 23, 2020 by Ralf Jung C-enhancement T-heap_lang
- CLOSED
- 1
- 0
updated May 25, 2020