Skip to content
GitLab
Explore
Sign in
Dan Frumin
iris-coq
Repository
Branches
Overview
Active
Stale
All
less_canonical
5226baf6
·
FAIL : Less canonical projections.
·
Feb 22, 2016
primitive_sealing
e7ff4737
·
Use primitive records for sealing.
·
Feb 25, 2016
ralf/magic-singleton
9bd5532f
·
demonstrate a weird issue
·
Mar 02, 2016
jh_inductive_pairs
7d2a0390
·
Failed attempt at improving performances of pairs by using inductives
·
Jun 16, 2016
atomic
16cfe6ce
·
Use telescopes for atomic triples.
·
Nov 23, 2016
state_inv
e6111441
·
Simplify wp_invariance.
·
Nov 24, 2016
ci
b9776424
·
CI
·
Nov 27, 2016
ralf/auth-frac
cf25cbc8
·
WIP: this is not nice. we should have a sigma-type-based auth instead.
·
Nov 30, 2016
list-agree
a64f7ac6
·
Kill dec_agree
·
Dec 01, 2016
coq-8.6
70cbc024
·
WIP: make OFEs and CMRAs use primitive projections
·
Dec 03, 2016
docs
54e7671c
·
IntoModal --> FromModal in the docs
·
Mar 16, 2017
pureexec2
82fdeb9e
·
Get rid of unnecessary unlocking in `solve_to_val`
·
Sep 25, 2017
pureexec
default
3a5c5045
·
Move some stuff.
·
Sep 25, 2017
boxed
34a3164b
·
Add a boxed barrier proof
·
Nov 23, 2017
bij
608f007c
·
Better names for base_logic.lib.bij
·
Nov 28, 2017
big_sepl_delete
7e12fbd3
·
Implement `big_sepL_delete`
·
Mar 27, 2018
to_agree_op
b1b6a661
·
Add `to_agree_op`
·
Apr 03, 2018
gmultiset
638b445b
·
gmultiset RA
·
Apr 11, 2018
Wclosed
e0d9d33d
·
Strengthen W.is_closed_correct.
·
Oct 11, 2018
patch-1
1465e070
·
Update the link to std++
·
Nov 16, 2018
Prev
1
2
3
Next