Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
Iris
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Model registry
Operate
Terraform modules
Monitor
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
Gaëtan Gilbert
Iris
Graph
4c34160115066eff12c4543d38ddc81801dd8539
Select Git revision
Branches
1
master
default
protected
1 result
You can move around the graph by using the arrow keys.
Begin with the selected commit
Created with Raphaël 2.2.0
6
Sep
30
Aug
29
28
27
26
25
24
22
16
14
13
12
9
8
7
6
30
Jul
22
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
27
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
16
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
Tweak names in proof.
Merge branch 'master' into 'master'
fix typo
formatting
bump std++
release 3.2.0
Merge branch 'ralf/changelog' into 'master'
add links
wording
short summary of main new features
prepare for 3.2: thank people
Merge branch 'feature/list_cmra_lemmas' into 'master'
added lemmas for list cmra
show that the empty type is a COFE and a CMRA
Merge branch 'big_op2_swap' into 'master'
Add `big_sepL2_swap`
Bump stdpp.
Merge branch 'robbert/big_op_commute' into 'master'
Add changelog entry.
Merge branch 'fill_reducible_no_obs' into 'master'
Apply suggestion to theories/program_logic/ectx_language.v
Move big_op lemmas for plainly to `plainly` file to be consistent w.r.t. other BI files.
Add `head_prim_fill_reducible_no_obs`
Refactor proofs for `|={E}=>` commuting with bigops, and make names consistent.
Show that `|==>` commutes with big ops (in one way).
Clearify `(pat1 & pat2 & .. & patn)` syntax.
update one_shot_once
bump std++
Bump stdpp.
Merge branch 'fix-direction-op-lemmas' into 'master'
Flip cmra_morphism_core
Flip cmra_morphism_pcore
Fix #256: Fix direction of f_op lemmas
Merge branch 'ralf/array' into 'master'
add timeless instance
comments
Merge branch 'robbert/issue260' into 'master'
Attempt at fixing compilation with Coq 8.7.2.
prepare for having fractional arrays in the future
Add test case.
Loading