Skip to content
GitLab
Explore
Sign in
Iris
Iris
Repository
Branches
Overview
Active
Stale
All
robbert/bi_cofe
00d2fb63
·
Ensure that different `Cofe` proofs of `iProp` are convertible.
·
Apr 07, 2022
!784
robbert/big_sepM2
d88db874
·
big_sepM2.
·
Mar 13, 2019
robbert/bupd_be_gone
d3814459
·
Remove basic updates from the Iris model, and define them using plainly.
·
Oct 27, 2018
robbert/clprop
506bd180
·
Add `cl_logic` folder to README.
·
Sep 05, 2020
robbert/docs_1_2_lemmas
c60d504d
·
More documentation about _1 and _2 lemmas.
·
Oct 18, 2023
!1008
robbert/fail_ofe_bi
9d533fdd
·
Failed experiment: put `ofe` directly in `bi`.
·
Apr 19, 2020
robbert/fupd_elim
97f90263
·
Make use of better `iMod` for updates.
·
Jan 05, 2021
robbert/has_lc_if
1fe85887
·
Add class `HasLcIf` so that it becomes easier to write generic adequacy lemmas.
·
Jul 06, 2022
robbert/hint_cut_plain
df44c4fe
·
Use `Hint Cut` for `Plain`.
·
May 05, 2023
robbert/iAssert_with
9835899b
·
Syntax `iAssert (Q with spat) as ...` which is consistent with `with`s elsewhere.
·
Feb 19, 2018
robbert/iIntro_iDestruct_fresh
20f36bef
·
More WIP.
·
Oct 04, 2023
!992
robbert/internal_fractional_tweaks
8de85872
·
Style tweaks to rwlocks.
·
Aug 28, 2023
!976
robbert/into_forall_eta
92d67959
·
Remove more etas.
·
Feb 16, 2024
!1020
robbert/issue_331
19671d2f
·
Test case.
·
Jun 29, 2020
robbert/level
9418cdd3
·
Use priority levels for `iFrame`. There's no syntax yet, so the fixes to the...
·
Oct 12, 2021
robbert/local_ltac_proofmode
908ae8f9
·
Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.
·
Jul 24, 2023
!953
robbert/lock_G_Σ
fa555c7b
·
Test that lock `Σ`s can be found in adequacy.
·
Aug 29, 2023
!980
robbert/lock_no_gamma
68e8477d
·
Get rid of γs in locks.
·
Jun 10, 2019
robbert/no_always_forall
60b3610c
·
Experiment: remove always_forall.
·
Aug 21, 2017
robbert/no_native_compute
93d9ef74
·
Avoid relying on native_compute.
·
Nov 16, 2022
!865
Prev
1
2
3
4
5
Next