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
952daeb93ba3b93c15c5b391f1d3ace88bebdeea
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
18
May
16
15
14
13
12
11
8
7
5
1
28
Apr
26
25
24
23
22
18
16
15
14
9
8
7
6
4
3
2
1
31
Mar
27
25
23
21
20
19
18
16
13
12
10
9
6
4
28
Feb
26
25
24
23
20
19
18
17
15
14
13
12
11
10
7
6
5
4
3
2
1
30
Jan
29
23
21
18
17
16
15
14
13
11
10
9
8
7
20
Dec
19
18
14
13
10
9
6
5
4
2
25
Nov
22
21
20
14
13
12
11
10
8
7
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
Coqify the comments.
Fix notation in comments
copy all gen_heap and gen_inv_heap mapsto lemmas, and name variables
CHANGELOG, update gen_inv_heap comment
define and prove array_free
add lifting lemma and tactic for single-location Free
add single-location Free operation to language syntax and semantics
note some design choices
make heap store (option val) in preparation for deallocation
document our breaking-changes-notification system
Merge branch 'ralf/inv_heap' into 'master'
changelog
exhaustive match for lit_is_unboxed
Merge branch 'use-lia' into 'master'
Use lia to avoid omega deprecation warnings
Merge branch 'robbert/twp_vals_compare_safe' into 'master'
Test cases.
Also use `solve_vals_compare_safe` in TWP case of `wp_pure`.
update a reference to long-gone double_neation module
make inv_heapG part of heapG
Merge branch 'big_sepL-inv' into 'master'
Add big_sepL2_nil_inv_l/r.
Merge branch 'ralf/lang-axioms' into 'master'
update dependencies
rename lemma variable names for more clarity
tweak wording
Add lemma `exist_wand_forall`, similar to `exist_impl_forall`.
tweak proof
tweak comments
explain our langauge axioms better
Merge branch 'ralf/select' into 'master'
update dependencies
use new select tactic from std++
update dependencies
build-all: test slow projects first and fast ones later
Merge branch 'core-id-local-update' into 'master'
Readd core_id_local_update
Update proofs
Combine intro patterns
Apply suggestion to theories/algebra/agree.v
Loading