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
George Pirlea
Iris
Repository graph
Repository graph
You can move around the graph by using the arrow keys.
5361ad82e1169177b26d6db6156cc5117b7afd11
Select Git revision
Branches
20
ci/3.1.0
ci/debug
ci/disable-ltac-backtrace
ci/for_proph
ci/janno/debug-opam
ci/janno/let_bind_envs
ci/janno/vmcast
ci/joe/compact_ipm
ci/joe/compact_ipm_remaining
ci/joe/compact_ipm_simple
ci/maximedenes/instance-nobody-open-proof
ci/mtac2-tt
ci/prophecy
ci/ralf/ci
ci/ralf/pm_red
ci/ralf/set_unfold_elements
ci/robbert/faster_iDestruct
ci/robbert/faster_iDestruct2
ci/robbert/faster_iFresh_joe
ci/robbert/into_val_pures
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
14
Jun
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
22
21
20
19
18
16
15
14
13
12
9
8
7
6
3
2
document WP format strings
Merge branch 'ralf/reftests' into 'gen_proofmode'
also test the output of error messages
Move local recursive ltac functions out to their own definitions to shorten backtraces
bump stdpp
allow FrameMonPredAt to infer the index
trigger an anomaly in Coq
ralf/coqbug/iAc…
ralf/coqbug/iAccu-anomaly
Merge branch 'ci/ralf/monpred-frame' into 'gen_proofmode'
make atomic_acc typeclasses-opaque
use IntoVal for alloc spec
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
make atomic_heap a typeclass and add some notation for it
Use telescopes for atomic accessors, updates and triples; add notation for all of them
Merge branch 'gen_proofmode' into ci/ralf/telescopes
forgot to update reference output
fix newlines being inserted in bad places for WP
Merge branch 'gen_proofmode' into ci/ralf/telescopes
fix yet another case of broken heap_lang notation
monpred test: use typed turnstile notation
monpred wand/impl framing: don't require indices to match syntactically
different approach to monPred framing
Stop timing on Coq 8.7
Fix inconsistent big operator instance names.
Typo in CHANGELOG.md
Merge branch 'gen_proofmode' into ci/ralf/telescopes
improve printing of texan triples
Merge branch 'fupd_step_wp' into 'gen_proofmode'
Update changlog.
Mask-changing updates that take a step.
Change WP so that we have an fupd before the later, but after the quantification over next states.
fix alignment
add a test for framing monPred_at below a wand
fix printing notation when importing heap_lang.lang after heap_lang.notation
remove unnecessary import
Plain typeclass should not require BiPlainly instance to be inferred
fix format spacing for texan triples
Loading