Skip to content
GitLab
Explore
Sign in
Overview
Active
Stale
All
ralf/sprop
2f143753
·
bump std++
·
Sep 06, 2021
ralf/f_equiv_ho
d72f8214
·
fix for f_equiv improvements
·
Sep 26, 2021
ralf/f_equiv
4f836b8e
·
adjust for f_equiv optimizations
·
Sep 27, 2021
robbert/level
9418cdd3
·
Use priority levels for `iFrame`. There's no syntax yet, so the fixes to the...
·
Oct 12, 2021
robbert/bi_cofe
00d2fb63
·
Ensure that different `Cofe` proofs of `iProp` are convertible.
·
Apr 07, 2022
!784
robbert/has_lc_if
1fe85887
·
Add class `HasLcIf` so that it becomes easier to write generic adequacy lemmas.
·
Jul 06, 2022
ralf/has-lc
cdfa27c0
·
track has_lc directly in invGS/irisGS/heapGS rather than via separate typeclass
·
Jul 15, 2022
ci/general-contractive
70df718a
·
generalize definition of contractiveness
·
Jul 29, 2022
robbert/add_sub
e1f9c08b
·
Port to std++.
·
Aug 10, 2022
ci/msammler/nb_state
4a4b3d53
·
Allow specifing states that are allowed to be stuck
·
Aug 11, 2022
ralf/make
297edd7f
·
add QuickPersistent, QuickIntuitionistic classes
·
Aug 16, 2022
ci/robbert/set_solver_eauto
336404e0
·
update to std++ snapshot
·
Oct 27, 2022
simon/parametric-index
64cd40ba
·
Merge branch 'master' into simon/parametric-index
·
Oct 27, 2022
robbert/no_native_compute
93d9ef74
·
Avoid relying on native_compute.
·
Nov 16, 2022
!865
ci/robbert/big_op_binder
0721fd0d
·
Document FIXME.
·
Nov 17, 2022
ralf/Z
1e37031b
·
get rid of Z.to_nat coercion, and add some Z-based APIs: big_sepL, and HeapLang arrays
·
Jan 12, 2023
!883
ralf/bi-persistently-emp
220dad25
·
Change `BiPersistentlyEmp` into `BiPersistentlyTrue`, which seems more natural.
·
Apr 28, 2023
robbert/pm_unify_class
221ce5ec
·
`Unify` type classes that factors out use of `notypeclasses refine` in proof mode classes.
·
Apr 30, 2023
!916
ci/hint-cut-revert
4069e553
·
Revert "Merge branch 'ralf/separable' into 'master'"
·
May 05, 2023
ci/ralf/options-timing
39e22b1f
·
Revert "re-export std++ options"
·
May 05, 2023
Prev
1
2
3
4
5
Next