Skip to content
GitLab
Explore
Sign in
Dan Frumin
iris-coq
Repository
Branches
Overview
Active
Stale
All
local_updates
fd3555d0
·
Add local update lemmas for `discrete_fun` and `unit`.
·
Jul 24, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
master
f6beee55
·
Merge branch 'master' into 'master'
·
Dec 30, 2021
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
is_closed_free_vars
4033848e
·
wip
·
Dec 11, 2021
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ofe_tweaks
9fb6751e
·
Add a `Proper` instance for ccompose.
·
May 27, 2021
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
big_sepM2_lemmata
41306b35
·
Simplify `big_sepM2_union_inv_l` proof significantly.
·
May 26, 2021
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
dfrumin-master-patch-71378
89c539ef
·
Fix typo in the comments.
·
Apr 29, 2021
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
patch-2
90231acd
·
Consistent meta-variables in CHANGELOG
·
Jul 06, 2020
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
big_sepL-inv
2156de4a
·
Use Robbert's proof
·
May 13, 2020
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
twp_array
cc67112b
·
Add twp_ lemmas for the arrays.
·
Feb 10, 2020
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
big_op2_swap
d1ecce0a
·
Swap the direction in the `_flip` big_op lemmas.
·
Aug 26, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
fill_reducible_no_obs
4dbfd13e
·
Apply suggestion to theories/program_logic/ectx_language.v
·
Aug 22, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
fresh_locs_arg
80623a8c
·
Get rid of a superflous argument to `fresh_locs`.
·
Jul 09, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
isimpl_test
63adcecf
·
Add an `iSimpl in "%"` test.
·
May 06, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
isimpl_many
a7fe86a3
·
Make the argument to `iEval` a selection pattern.
·
May 01, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
changelog_upd
b12759c2
·
Mentioned big_sepL2/sepM2 in the changelog.
·
Apr 07, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/big_sepM2
8c367063
·
`nil` -> `empty` for some big_ops
·
Mar 29, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
resolve_proph_fix
5e9a8aed
·
Remove unnecessary arguments from `ResolveProphS`.
·
Mar 20, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
own_alloc_infinite
843bf221
·
Implement `own_alloc_infinite`
·
Mar 06, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ispecialize_pers
46f4ae77
·
Make `iSpecialize ("H" with "[#]")` produce a persistent result.
·
Feb 16, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
option_mbind_ne
b225ccb1
·
Monadic bind & join for `option` are non-expansive.
·
Feb 05, 2019
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
Prev
1
2
3
Next