Skip to content
GitLab
Explore
Sign in
Iris
Iris
Repository
Branches
Overview
Active
Stale
All
master
default
protected
5ae02407
·
update dependencies
·
Apr 19, 2024
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/reservation_map_False
0dafeb83
·
WIP.
·
Mar 14, 2024
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/into_forall_eta
92d67959
·
Remove more etas.
·
Feb 16, 2024
!1020
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/timing
00dad6b9
·
benchmark a different branch
·
Oct 24, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/docs_1_2_lemmas
c60d504d
·
More documentation about _1 and _2 lemmas.
·
Oct 18, 2023
!1008
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/affine_notations
e8a163c1
·
Add notations for `<affine> ⌜ ⌝` and friends.
·
Oct 15, 2023
!1007
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/sbi
f11da827
·
WIP; split up into reasonably sized commits.
·
Oct 08, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
jh/simplify_na_inv
20bb7cc3
·
Simplify NA-inv protocol.
·
Oct 06, 2023
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
robbert/iIntro_iDestruct_fresh
20f36bef
·
More WIP.
·
Oct 04, 2023
!992
Select Archive Format
Download source code
zip
tar.gz
tar.bz2
tar
ci/name-mangle
46e8f68d
·
enable name mangling
·
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
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
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
Prev
1
2
3
4
5
Next