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
322cdf378fa480517c5831a66ea6022b3b7c229a
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
7
Nov
6
5
2
1
31
Oct
25
22
18
14
12
11
9
6
20
Sep
19
13
11
9
8
6
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
Merge branch 'ci/robbert/hintmode_inG' into 'master'
Set `Hint Mode` for `inG`.
switch to new ocaml default compiler
switch timing to Coq 8.10.1
also clean top-level lia.cache
Bump std++.
Lemmas to show that `monPred`s are persistent/absorbing/affine.
Stylistic tweaks in `monPred`.
More sensible instance names for `monPred`'s `BiAffine` and `BiPositive`.
Move `monPred_at` lemmas up, so we can use them for other lemmas.
Merge branch 'lang_lemmas' into 'master'
Lang lemmas
Remove useless scope.
Simplify definition of cancelable invariants.
Merge branch 'cinv_open_stronger' into 'master'
Added a stronger version of cinv_open_strong
Use `core` database.
Merge branch 'robbert/invariants' into 'master'
Simplify definition of invariant model.
Minor tweaks in lifting file.
only run CI on parent repo
Merge branch 'fix-gitignore' into 'master'
Update gitignore
Bump stdpp.
Merge branch 'ralf/docs' into 'master'
move docs around
Merge branch 'ralf/ambig-coerc' into 'master'
make gFunctors_lookup not longer a coercion
Merge branch 'patch-readme' into 'master'
Update version in URL for Iris appendix
Merge branch 'robbert/internal_eq_soundness' into 'master'
Soundness lemma for internal equality of `uPred`.
add coq support changes to changelog
Merge branch 'ralf/sem-inv' into 'master'
add changelog
Merge branch 'ralf/drop-old-coq' into 'master'
drop Coq 8.7 and add 8.10
style improvements
semantic invariants
Merge branch 'ralf/poison' into 'master'
Loading