Issues · Iris / Iris

New issue

Typeclass inference fails to trigger.

#346 · opened 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 · opened Sep 10, 2020 by Robbert
- CLOSED
- 8
updated Sep 12, 2020
Missing {u,}rFunctors and conversions

#342 · opened Aug 20, 2020 by Paolo G. Giarrusso A-coq C-enhancement T-algebra
- CLOSED
- 1
- 1
updated Sep 10, 2020
Use a "settings" file for setting options within the project

#66 · opened Jan 21, 2017 by Ralf Jung A-infra C-enhancement
- CLOSED
- 2
- 17
updated Sep 10, 2020
Remove eta-expansions from sealed definitions

#285 · opened Jan 15, 2020 by Ralf Jung A-coq C-enhancement T-style
- CLOSED
- 1
- 0
updated Aug 30, 2020
Drop support for Coq 8.9?

#318 · opened May 12, 2020 by Ralf Jung A-coq
- CLOSED
- 1
- 2
updated Aug 24, 2020
Use user-supplied names in iIntros (?)

#336 · opened Jul 20, 2020 by Tej Chajed
- CLOSED
- 1
- 3
updated Aug 12, 2020
Weird automatically generated names

#337 · opened Jul 22, 2020 by Robbert
- CLOSED
- 1
- 2
updated Aug 12, 2020
Iris Library Best Practices

#333 · opened Jul 07, 2020 by Ralf Jung A-docs
- CLOSED
- 1
- 1
updated Aug 06, 2020
Port HeapLang tactics to more efficient style

#315 · opened Apr 29, 2020 by Robbert A-coq C-enhancement I-performance T-heap_lang
- CLOSED
- 1
- 0
updated Jul 15, 2020
Iris 3.3 release planning 8 of 8 tasks completed

#306 · opened Apr 07, 2020 by Ralf Jung Iris 3.3 A-coq C-project
- CLOSED
- 1
updated Jul 15, 2020
Use Coq deprecation attribute to implement deprecations

#296 · opened Feb 29, 2020 by Tej Chajed Iris 3.3 A-coq C-enhancement
- CLOSED
- 1
- 1
- 0
updated Jul 15, 2020
Fix name duplication `elem_of_list_singleton` in Iris and std++

#309 · opened Apr 07, 2020 by Robbert Iris 3.3 A-coq C-bug T-algebra
- CLOSED
- 1
- 18
updated Jul 15, 2020
iSpecialize with "[% //]" does not report an error if done fails

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

#324 · opened 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 · opened May 28, 2020 by Dmitry Khalanskiy
- CLOSED
- 4
updated May 28, 2020
Add deallocation operation to HeapLang

#313 · opened Apr 23, 2020 by Ralf Jung C-enhancement T-heap_lang
- CLOSED
- 1
- 0
updated May 25, 2020
Notation `(⊢@{PROP})` and `(⊣⊢@{PROP} )` broken

#302 · opened Mar 30, 2020 by Robbert A-coq C-bug T-bi
- CLOSED
- 2
- 12
updated May 24, 2020
Fix "omega is deprecated" warnings by switching to lia

#319 · opened May 16, 2020 by Tej Chajed
- CLOSED
- 1
- 2
updated May 16, 2020
Follow-up from "Lang lemmas": intuitive explanation of mixin_step_by_val

#271 · opened Nov 06, 2019 by Ralf Jung Iris 3.3 A-theory C-enhancement T-heap_lang
- CLOSED
- 1
- 0
updated May 13, 2020