Skip to content
GitLab
Projects
Groups
Topics
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Iris
Iris
Repository
Branches
Overview
Active
Stale
All
ci/name-mangle
46e8f68d
·
enable name mangling
·
Sep 29, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/timing
4abdc826
·
timing with Coq 8.17
·
Sep 29, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
master
default
protected
4f3a385f
·
add 'iris-bot timing all'
·
Sep 29, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/lock_G_Σ
fa555c7b
·
Test that lock `Σ`s can be found in adequacy.
·
Aug 29, 2023
!980
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/internal_fractional_tweaks
8de85872
·
Style tweaks to rwlocks.
·
Aug 28, 2023
!976
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ralf/ra-infer
bd80b71c
·
experiment: use coq's ability to infer more canonical structures
·
Aug 11, 2023
!972
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ralf/iso_cmra
8ecf601f
·
generalize iso_cmra_mixin_restrict to a lemma that can also restrict the domain
·
Aug 10, 2023
!970
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ralf/fmap_dist_inj
8d59d7a5
·
add option_fmap_dist_inj lemma
·
Aug 10, 2023
!969
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ralf/solve-proper-subrelation
188132d2
·
have solve_proper exploit OfeDiscrete and LeibnizEquiv
·
Aug 08, 2023
!968
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ralf/gmap_view_cmra
b579fafb
·
port the rest of Iris to the new gmap_view
·
Jul 27, 2023
!959
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/local_ltac_proofmode
908ae8f9
·
Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.
·
Jul 24, 2023
!953
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/sbi
009bbd9b
·
Remove useless `BiAffine` premises for `Plain` of big ops.
·
Jul 09, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
coq-bugs/tc-resolution-cannot-unify-with-self
a1abaf74
·
reproducer for Coq bug
·
Jun 04, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/robbert/hint_cut_plain
df44c4fe
·
Use `Hint Cut` for `Plain`.
·
May 05, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/hint_cut_plain
df44c4fe
·
Use `Hint Cut` for `Plain`.
·
May 05, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/ralf/options-timing
39e22b1f
·
Revert "re-export std++ options"
·
May 05, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/hint-cut-revert
4069e553
·
Revert "Merge branch 'ralf/separable' into 'master'"
·
May 05, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/pm_unify_class
221ce5ec
·
`Unify` type classes that factors out use of `notypeclasses refine` in proof mode classes.
·
Apr 30, 2023
!916
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ralf/bi-persistently-emp
220dad25
·
Change `BiPersistentlyEmp` into `BiPersistentlyTrue`, which seems more natural.
·
Apr 28, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/resolve_tc
9fe5d81c
·
Use `resolve_tc` and remove all uses of "legacy" `apply` in Iris Proof Mode.
·
Apr 18, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
Prev
1
2
3
4
5
Next