Skip to content
GitLab
Explore
Sign in
Pierre Roux
Iris
Repository
Branches
Overview
Active
Stale
All
coq_18928
8c11e613
·
exclude Coq 8.20 from printing tests
·
Apr 16, 2024
master
default
protected
9cb4b4a5
·
Merge branch 'ralf/old-coq' into 'master'
·
Feb 05, 2024
ralf/token
e45b38fa
·
token: support iCombine ... gives
·
Jan 23, 2024
robbert/into_forall_eta
3533a0d3
·
Add test case.
·
Nov 15, 2023
ci/timing
00dad6b9
·
benchmark a different branch
·
Oct 24, 2023
robbert/docs_1_2_lemmas
c60d504d
·
More documentation about _1 and _2 lemmas.
·
Oct 18, 2023
robbert/affine_notations
e8a163c1
·
Add notations for `<affine> ⌜ ⌝` and friends.
·
Oct 15, 2023
robbert/sbi
f11da827
·
WIP; split up into reasonably sized commits.
·
Oct 08, 2023
jh/simplify_na_inv
20bb7cc3
·
Simplify NA-inv protocol.
·
Oct 06, 2023
robbert/iIntro_iDestruct_fresh
20f36bef
·
More WIP.
·
Oct 04, 2023
ci/name-mangle
46e8f68d
·
enable name mangling
·
Sep 29, 2023
robbert/lock_G_Σ
fa555c7b
·
Test that lock `Σ`s can be found in adequacy.
·
Aug 29, 2023
robbert/internal_fractional_tweaks
8de85872
·
Style tweaks to rwlocks.
·
Aug 28, 2023
ralf/ra-infer
bd80b71c
·
experiment: use coq's ability to infer more canonical structures
·
Aug 11, 2023
robbert/local_ltac_proofmode
908ae8f9
·
Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.
·
Jul 24, 2023
coq-bugs/tc-resolution-cannot-unify-with-self
a1abaf74
·
reproducer for Coq bug
·
Jun 04, 2023
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
ci/ralf/options-timing
39e22b1f
·
Revert "re-export std++ options"
·
May 05, 2023
ci/hint-cut-revert
4069e553
·
Revert "Merge branch 'ralf/separable' into 'master'"
·
May 05, 2023
Prev
1
2
3
4
5
Next