Merge Requests · Iris · GitLab

Make EqType more realistic

examples!4 · opened Mar 21, 2018 by Amin Timany
- MERGED
- 8
updated Jan 25, 2019
Store a counter in `Envs` to assign fresh names with `iFresh`.

iris!128 · opened Mar 12, 2018 by Joseph Tassarotti gen_proofmode
- MERGED
- 10
updated Mar 15, 2018
`Cancelable` instances for all elements of option/gmap

iris!127 · opened Mar 04, 2018 by Robbert Krebbers
- MERGED
- 4
updated Oct 04, 2018
Renaming and notations for modalities gen_proofmode

iris!126 · opened Mar 04, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 5
updated Mar 04, 2018
Bundle classes for updates, plainly and embeddings

iris!125 · opened Mar 02, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 50
updated Mar 03, 2018
Make iFrame able to accumulate assertions in an evar.

iris!124 · opened Mar 01, 2018 by Jacques-Henri Jourdan gen_proofmode
- MERGED
- 10
updated Mar 03, 2018
Get rid of `FromLaterN` class.

iris!123 · opened Mar 01, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 15
updated Mar 03, 2018
Use `<:` (VMcast) for instances of `exact I` in lang/tactics.v

lambda-rust!10 · opened Feb 28, 2018 by Janno
- MERGED
- 13
updated Mar 01, 2018
Repair the plainly modality

iris!122 · opened Feb 23, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 1
- 32
updated Feb 26, 2018
Super `iModIntro` tactic that generalizes `iAlways`, `iNext`, `iModIntro`, and more 7 of 7 tasks completed

iris!121 · opened Feb 23, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 35
updated Jul 13, 2018
Fix regression in iGPS caused by eebe055b958d6db12ef5ccd2718bc3c952438483.

iris!120 · opened Feb 22, 2018 by Robbert Krebbers
- MERGED
- 3
updated Feb 23, 2018
weaken BI axiom persistently_and_sep_elim and re-derive the stronger form

iris!119 · opened Feb 21, 2018 by Ralf Jung gen_proofmode
- MERGED
- 0
updated Feb 21, 2018
Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type.

iris!118 · opened Feb 20, 2018 by Jacques-Henri Jourdan
- MERGED
- 5
updated Feb 20, 2018
General Invariant Tactic

iris!116 · opened Feb 16, 2018 by Joseph Tassarotti gen_proofmode
- MERGED
- 81
updated Jul 13, 2018
Set mode for update modalities

iris!115 · opened Feb 13, 2018 by Ralf Jung gen_proofmode T-proofmode
- MERGED
- 32
updated Feb 14, 2018
Make `FromPure` depend on an affinity parameter

iris!114 · opened Feb 12, 2018 by Jacques-Henri Jourdan gen_proofmode T-proofmode
- MERGED
- 4
updated Jul 13, 2018
Bring back side-conditionals for `iMod`

iris!113 · opened Feb 12, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 7
updated Feb 15, 2018
Add a `NoBackTrack` type class.

stdpp!27 · opened Feb 08, 2018 by Robbert Krebbers
- MERGED
- 0
updated Feb 09, 2018
Use `NoBackTrack` type class for framing with ▷ 1 of 1 task completed

iris!112 · opened Feb 08, 2018 by Robbert Krebbers
- MERGED
- 15
updated Feb 08, 2018
A simple type class based canceler for natural numbers.

stdpp!26 · opened Feb 07, 2018 by Robbert Krebbers
- MERGED
- 5
updated Feb 08, 2018

Prev
1
…
36
37
38
39
40
41
42
43
44
…
46
Next