Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
T
transfinite
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Simon Spies
transfinite
Graph
14eb9f857f8c4283ed73ce3784c419e939d00443
Select Git revision
Branches
5
core
master
default
protected
new_master
simon/parametric-index
step-index-class
5 results
You can move around the graph by using the arrow keys.
Begin with the selected commit
Created with Raphaël 2.2.0
9
Sep
14
Apr
8
Dec
28
Nov
24
22
Jul
14
13
12
9
7
5
3
1
30
Jun
29
28
27
26
25
24
21
20
19
18
17
16
15
14
13
12
11
10
9
7
6
5
4
3
2
1
31
May
30
29
28
26
25
24
23
21
20
19
16
15
13
12
9
8
7
6
4
2
1
30
Apr
29
27
26
25
24
23
17
8
7
29
Mar
26
22
20
19
17
16
15
14
13
7
6
5
4
3
1
28
Feb
27
26
25
24
23
22
21
20
18
16
13
7
6
5
3
1
30
Jan
29
28
27
26
25
24
23
22
19
18
17
15
14
13
11
10
2
25
Dec
22
21
20
19
18
15
14
13
12
10
8
7
6
3
30
Nov
29
28
27
26
22
20
16
12
11
9
8
6
1
31
Oct
29
27
26
25
24
22
21
19
18
13
11
7
5
4
3
30
Sep
26
18
12
outdated files from another version
remove examples and instances
remove old options file in algebra
new versions of the step-indexing files
add iris prelude
update coq project and opam
update license
master
master
gstep rule
Update README.md
use non-timing runner
add CI back in
rebase transfinite iris
new_master
new_master
mention how to use iLöb for recursive functions
Merge branch 'big_sepL2_app_inv_2' into 'master'
Rename `big_sepL2_app_inv_2` -> `big_sepL2_app_inv`.
Merge branch 'head_prim_fill_reducible' into 'master'
Add `head_prim_fill_reducible`.
Merge branch 'sigTO_proper_projs' into 'master'
Mark projections for sigTO as NonExpansive and Proper
proper link and less Rust ;)
erasure is in iris/examples
Weaken premise of `gmultiset_local_update_dealloc`.
Merge branch 'ralf/pair-core' into 'master'
shorten proof
tweak proof to also work after a Coq bugfix
changelog for comparison changes
dont quantify over empty telescopes
Merge branch 'fresh_locs_arg' into 'master'
Get rid of a superflous argument to `fresh_locs`.
bump std++
show that pair cosntruction commutes with taking the core
Bump stdpp.
Add lemma `big_sepL2_reverse`.
Merge branch 'ralf/update' into 'master'
Stronger local update for multisets that entails the old ones.
Add lemmas for `≼` of `Cinl` and `Cinr`.
provide a lemma to update only the authoritative part, ignoring the fragments entirely
Merge branch 'ralf/eq' into 'master'
Make `iPure` non-local so it can be used for defining custom `iDestruct`-like tactics.
use decide instead of bool_decide where possible
Loading