Skip to content
GitLab
Explore
Sign in
Dan Frumin
iris-coq
Repository
Branches
Overview
Active
Stale
All
gmap_empty_included
efb33fdb
·
Add gmap.empty_included.
·
Dec 21, 2018
subst_map_closed
fafc06fe
·
Lemmas about subst_map on closed expressions
·
Dec 21, 2018
binder-insert
5ff0780b
·
Two small lemmas about binder_insert
·
Dec 18, 2018
patch-1
1465e070
·
Update the link to std++
·
Nov 16, 2018
Wclosed
e0d9d33d
·
Strengthen W.is_closed_correct.
·
Oct 11, 2018
gmultiset
638b445b
·
gmultiset RA
·
Apr 11, 2018
to_agree_op
b1b6a661
·
Add `to_agree_op`
·
Apr 03, 2018
big_sepl_delete
7e12fbd3
·
Implement `big_sepL_delete`
·
Mar 27, 2018
bij
608f007c
·
Better names for base_logic.lib.bij
·
Nov 28, 2017
boxed
34a3164b
·
Add a boxed barrier proof
·
Nov 23, 2017
pureexec
default
3a5c5045
·
Move some stuff.
·
Sep 25, 2017
pureexec2
82fdeb9e
·
Get rid of unnecessary unlocking in `solve_to_val`
·
Sep 25, 2017
docs
54e7671c
·
IntoModal --> FromModal in the docs
·
Mar 16, 2017
coq-8.6
70cbc024
·
WIP: make OFEs and CMRAs use primitive projections
·
Dec 03, 2016
list-agree
a64f7ac6
·
Kill dec_agree
·
Dec 01, 2016
ralf/auth-frac
cf25cbc8
·
WIP: this is not nice. we should have a sigma-type-based auth instead.
·
Nov 30, 2016
ci
b9776424
·
CI
·
Nov 27, 2016
state_inv
e6111441
·
Simplify wp_invariance.
·
Nov 24, 2016
atomic
16cfe6ce
·
Use telescopes for atomic triples.
·
Nov 23, 2016
jh_inductive_pairs
7d2a0390
·
Failed attempt at improving performances of pairs by using inductives
·
Jun 16, 2016
Prev
1
2
3
Next