Merge Requests · Iris

👻 notation for `own`. 0 of 1 task completed

iris!233 · created Apr 09, 2019 by Robbert Krebbers
- CLOSED
- 5
- 5
updated Apr 23, 2019
Fix duplicate clear warning from occurrence switch

iris!243 · created May 08, 2019 by Tej Chajed
- CLOSED
- 6
updated May 08, 2019
WIP: Give sufficient condition on cameras for swapping ▷ with implication →, wand -*, and basic updates |==>

iris!231 · created Apr 01, 2019 by Paolo G. Giarrusso
- CLOSED
- 12
updated May 28, 2019
WIP: Make proof mode terms more compact

iris!224 · created Mar 14, 2019 by Joseph Tassarotti
- CLOSED
- 28
updated Jun 06, 2019
The Tactic Notation entry simple_intropattern now binds to Coq simple_intropattern.

iris!260 · created Jun 08, 2019 by Hugo Herbelin
- CLOSED
- 6
updated Jun 11, 2019
Add heap_lang library for resolve on CAS.

iris!271 · created Jun 15, 2019 by Rodolphe Lepigre
- CLOSED
- 14
updated Jun 17, 2019
WIP ltac_tactics.v show `lazy_tc` does not work

iris!272 · created Jun 15, 2019 by Paolo G. Giarrusso
- CLOSED
- 2
updated Jun 18, 2019
WIP: simplified rdcss example

examples!21 · created Jun 17, 2019 by Gaurav Parthasarathy
- CLOSED
- 29
updated Jun 24, 2019
introduce notation for value comparison

iris!279 · created Jun 21, 2019 by Ralf Jung Iris 3.2
- CLOSED
- 8
updated Jun 29, 2019
Fix direction of CONSTRUCTOR_NAME_op lemmas (fix #256)

iris!295 · created Jul 22, 2019 by Paolo G. Giarrusso
- CLOSED
- 20
updated Aug 13, 2019
Avoid relying on `Export` bugs

stdpp!92 · created Sep 05, 2019 by Maxime Dénès
- CLOSED
- 3
updated Sep 05, 2019
Avoid relying on `Export` bugs

iris!312 · created Sep 10, 2019 by Maxime Dénès
- CLOSED
- 7
updated Sep 13, 2019
Avoid relying on `Export` bugs

lambda-rust!14 · created Sep 10, 2019 by Maxime Dénès
- CLOSED
- 2
updated Sep 15, 2019
Semantic Invariants

iris!290 · created Jul 12, 2019 by Simon Spies
- CLOSED
- 19
updated Nov 01, 2019
Persistently: Get rid of mono and idemp in favor of intro

iris!102 · created Dec 19, 2017 by Ralf Jung
- CLOSED
- 22
updated Nov 01, 2019
WIP: Strong framing

iris!50 · created Feb 18, 2017 by Robbert Krebbers T-proofmode
- CLOSED
- 31
updated Nov 01, 2019
Adapting to Coq PR#10832: formats associated to a given interpretation not taken into account

iris!335 · created Nov 12, 2019 by Hugo Herbelin
- CLOSED
- 7
updated Nov 13, 2019
Use `class_apply` instead of `refine` to avoid unwanted evars

iris!342 · created Dec 12, 2019 by Maxime Dénès
- CLOSED
- 4
updated Dec 12, 2019
Make fupd_proper more convenient to use (fix #284)

iris!353 · created Jan 04, 2020 by Paolo G. Giarrusso
- CLOSED
- 1
updated Jan 04, 2020
when the goal is an evar, pick emp when possible

iris!139 · created Apr 20, 2018 by Ralf Jung gen_proofmode
- CLOSED
- 2
updated Jan 31, 2020