Skip to content
GitLab
Explore
Sign in
Overview
Active
Stale
All
ci/robbert/hint_cut_plain
df44c4fe
·
Use `Hint Cut` for `Plain`.
·
May 05, 2023
robbert/hint_cut_plain
df44c4fe
·
Use `Hint Cut` for `Plain`.
·
May 05, 2023
coq-bugs/tc-resolution-cannot-unify-with-self
a1abaf74
·
reproducer for Coq bug
·
Jun 04, 2023
robbert/local_ltac_proofmode
908ae8f9
·
Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.
·
Jul 24, 2023
!953
ralf/ra-infer
bd80b71c
·
experiment: use coq's ability to infer more canonical structures
·
Aug 11, 2023
!972
robbert/internal_fractional_tweaks
8de85872
·
Style tweaks to rwlocks.
·
Aug 28, 2023
!976
robbert/lock_G_Σ
fa555c7b
·
Test that lock `Σ`s can be found in adequacy.
·
Aug 29, 2023
!980
ci/name-mangle
46e8f68d
·
enable name mangling
·
Sep 29, 2023
robbert/iIntro_iDestruct_fresh
20f36bef
·
More WIP.
·
Oct 04, 2023
!992
jh/simplify_na_inv
20bb7cc3
·
Simplify NA-inv protocol.
·
Oct 06, 2023
robbert/sbi
f11da827
·
WIP; split up into reasonably sized commits.
·
Oct 08, 2023
robbert/affine_notations
e8a163c1
·
Add notations for `<affine> ⌜ ⌝` and friends.
·
Oct 15, 2023
!1007
robbert/docs_1_2_lemmas
c60d504d
·
More documentation about _1 and _2 lemmas.
·
Oct 18, 2023
!1008
ci/timing
00dad6b9
·
benchmark a different branch
·
Oct 24, 2023
robbert/into_forall_eta
92d67959
·
Remove more etas.
·
Feb 16, 2024
!1020
robbert/reservation_map_False
0dafeb83
·
WIP.
·
Mar 14, 2024
Prev
1
2
3
4
5
Next