Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
iris-coq
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
Michael Sammler
iris-coq
Graph
80e3bc3116673c314c70adc3852099c21dd492c7
Select Git revision
Branches
20
atomic
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
fast_string
iris-3.0
iris-3.1
janno/metacoq
jh/done_contradiction
jh/evar_iframe
jh/independent_metric
jh/sprop_upred
jh_inductive_pairs
joe/bupd_derived
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
You can move around the graph by using the arrow keys.
Begin with the selected commit
Created with Raphaël 2.2.0
1
Aug
31
Jul
24
23
19
18
17
13
9
7
6
5
4
3
2
30
Jun
29
28
26
25
23
22
21
20
19
18
17
16
15
14
13
12
11
10
9
8
7
6
5
4
3
1
31
May
30
29
28
27
25
24
23
20
18
17
15
14
11
10
9
8
7
4
3
2
30
Apr
29
28
27
26
25
24
23
22
21
20
19
18
12
11
10
9
6
5
4
3
31
Mar
30
28
27
24
22
21
20
19
17
16
15
14
13
12
11
9
8
7
6
5
4
3
2
1
28
Feb
27
26
25
24
23
bumped Mtac2's commit
adapting to last change in Mtac2/master
Back to Mtac2/master.
Use Mtac2/janno/cps_unify.
CI issue was upstream in opam, partially revert the changes
update CI
update CI
Fix typo in comment.
Clarify comment.
Support `iInduction ... using`; this closes issue #204.
Merge branch 'insert_alloc_local_update' into 'master'
Added a new lemma to allocate fragmented ownership in unital gmaps while updating the full ownership
Update README.md even more
Update README.md
more MoSeL
bump std++; update test suite makefile
Bump Mtac2 commit.
Revert "Make heap_lang/proofmode.v universe polymorphic."
Make heap_lang/proofmode.v universe polymorphic.
Revert "Make heap_lang/tactics.v universe polymorphic."
Make heap_lang/tactics.v universe polymorphic.
Make proofmode/tactics.v polymorphic.
clean better
Merge branch 'ci/ralf/atomic' into 'master'
add iGPS to list of case studies we maintain
changelog
the rewrite problem now has an issue number
define a general make_laterable construct and use it for atomic updates
add lemma to prove atomic WP without seeing a Q
Sequential triples with a persistent precondition and no initial quantifier are atomic
add a tactic for the final introduction of an atomic accessor
enable iMod to run an atomic update
add a weak increment operation that knows it does not race
Prove that atomic triples imply "normal" triples
Add some lemmas about mapsto to the atomic_heap interface; use IntoVal for alloc spec
also test Coq 8.8.1
make atomic_heap a typeclass and add some notation for it
Use telescopes for atomic accessors, updates and triples; improve mask handling; add notation for all of them
bring CI back to normal
Merge branch 'gen_proofmode' into 'master'
Loading