Issues · Iris / Iris · GitLab

Decouple framing and IntoSep

#351 · opened Sep 29, 2020 by Ralf Jung A-coq C-enhancement I-performance T-proofmode
- 1
updated Sep 29, 2020
Make `contractive_proper` into a lemma, or control other instances that make it costly.

#321 · opened May 27, 2020 by Paolo G. Giarrusso A-coq C-enhancement I-performance T-algebra
- 1
- 1
updated Oct 20, 2020
Use `byte` based strings for proof mode

#317 · opened May 12, 2020 by Robbert A-coq C-enhancement I-performance T-proofmode
- 1
- 7
updated May 16, 2020
Canonical structures have major performance impact

#303 · opened Apr 05, 2020 by Robbert A-coq C-enhancement I-performance T-bi
- 17
updated May 11, 2020
Guide typeclass search via more specialized typeclasses

#298 · opened Mar 06, 2020 by Michael Sammler A-coq C-enhancement I-performance
- 2
updated Jun 17, 2020
Fix performance regressions in Iris and std++ in Coq 8.10.1 compared to Coq 8.9.0

#272 · opened Nov 07, 2019 by Robbert A-coq I-performance
- 14
updated Feb 12, 2020
Seal off local and frame-preserving update

#203 · opened Jul 05, 2018 by Ralf Jung A-coq C-enhancement I-performance T-algebra
- 0
updated Nov 01, 2019
eauto very slow when there is a chain of Iris quantifiers

#188 · opened May 23, 2018 by Ralf Jung A-coq C-bug I-performance T-proofmode
- 1
updated Nov 01, 2019
Explore performance implications of gen_proofmode

#180 · opened Apr 10, 2018 by Ralf Jung A-coq C-project I-performance T-proofmode
- 3
updated Nov 01, 2019
String-free proofterms

#172 · opened Mar 10, 2018 by Ralf Jung A-coq C-project I-performance T-proofmode
- 6
updated Sep 08, 2020