Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
iris
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
Tej Chajed
iris
Repository graph
Repository graph
You can move around the graph by using the arrow keys.
29c117af02bc2fa30866a4b2dc933e57b0d68f2a
Select Git revision
Branches
20
adjust-focused-goal
atomic
avoid-deprecated-arith
byte-strings
bytes-ident
ci/3.1.0
ci/debug
ci/janno/debug-opam
ci/janno/vmcast
ci/ralf/ci
ci/ralf/pm_red
ci/robbert/into_val_pures
ci/stability
ci/value_constructor
cmra-iso
cmra-restrict-valid
coqide-unicode-config
dfrac-smart-constructor
dfrac-valid-arg
document-ipm-classes
Tags
10
iris-3.1.0
iris-3.0.0
iris-2.0
iris-2.0-rc2
iris-2.0-rc1
iris-1.1
iris-1.0
hope-2015-coq-1
appendix-1.0.0
appendix-1
30 results
Begin with the selected commit
Created with Raphaël 2.2.0
24
Jun
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
13
12
11
9
8
6
1
31
Oct
29
27
26
25
24
22
21
20
19
18
13
12
11
10
7
5
4
remove some unnecessary scope annotations
avoid use of heap_lang notation in proofmode.v
avoid using value notation for primitive operational rules
add to CHANGELOG
comment nits
rename CompareExchange to CmpXchg
consistently annotate types for prophecy variables and lists
remove some unneeded type annotations
use equality instead of let binding
make primitive compare-exchange return both boolean and old value for ease of use
add 'atomic triple' for compare-and-set, and use it in one example
add lemmas for combining CAS and Resolve
turn CAS into compare-and-swap instead of compare-and-set: make it return the old value
disable some notation for now
more consistent order and format for CHANGELOG
Merge branch 'sigT-cFunctor' into 'master'
Reduce use of UIP as suggested by Robbert
Cofe and cFunctor for sigT
Merge branch 'fix-sed-mac-really' into 'master'
Fix instructions for Mac (and change them for Linux)
Bump stdpp.
Have `iNext` turn `Next x ≡ Next y` into `x ≡ y`.
Set `Hint Mode` for `Cofe`.
bump std++ (this contains ONLY the solve_ndisj change)
bump std++
Merge branch 'clairvoyant' into 'master'
Add clairvoyant_coin example
Merge branch 'stuck_fill' into 'master'
Make proof clear.
Add stuck_fill lemma.
CHANGELOG: comparison change
export solve_vals_cas_compare_safe
make cas_offset_vec lemmas more consistent
fix merge fallout
Merge branch 'ralf/eq' into 'master'
fix sed for macOS
Add C→O rename to CHANGELOG.
Bump stdpp.
Some forgotten C→O renames.
Merge branch 'robbert/ofe_rename' into 'master'
Loading