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
Marianna Rapoport
iris-coq
Graph
c55672d80427fb6e3073204cf62fd1f30ae25c35
Select Git revision
Branches
20
atomic
ci/janno/vmcast
ci/ralf/atomic
ci/ralf/lia
ci/ralf/pm_red
ci/ralf/telescopes
fast_string
gen_proofmode
iris-3.0
iris-3.1
janno/metacoq
jh/done_contradiction
jh/evar_iframe
jh/independent_metric
jh/sprop_upred
jh_inductive_pairs
joe/defined_pers
less_canonical
less_canonical_new
marianna/prophecy
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
Mar
29
Feb
28
27
26
25
24
23
22
21
20
19
18
17
16
15
14
13
12
11
10
9
8
5
4
3
2
1
31
Jan
forgot to ammend this...
fix name of recv_strengthen to recv_weaken
Load should bind more strongly than app.
Use "R"-suffixes for CMRA instances.
strengthen recv_split: no more skip
docs: tying the list of authors to one of the iris papers is rather silly
fix the docs
prove "THE CLIENT"
prove a weaker derived form of recv_strengthen; more "\lam:" notation
rename: minus -> div. Also change notation accordingly.
simplify cauchy condition on chains
preparations for describing agreement in The Iris Documentation
complete description of COFEs
wording
move some explanations from iris 2.0 paper to here
some tex nits
newchan -> newbarrier
Replace occurences of -> by →.
Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq
Notation for Case that is consistent with the constructor names.
make auth_fsa consistent about const-valid vs uPred-valid
prove a lemma for splitting \mapsto
be more explicit in From...Require becuase PG does not support this completely yet :-/
Improve notation for Case.
Hint Resolve for X ⊆ ⊤.
Fallthrough instance for heap lang substitution.
Language notations for Pair and Case.
New mechanism for heap_lang substitutions.
Make wp_rec/wp_lam solve to_of_val premises.
Add space to pretty printed notation ;; for seq.
Fractional heap.
Lemma for validity of Some.
Make discrete_cmra_discrete global.
Some decidable agreement CMRA properties.
Destructor for dec_agree.
Correct implicit arguments dec_agree.
Clean up names in excl.
Add fractional CMRA.
Add type for positive rationals.
Tweak implicit arguments of CMRAMonotone.
Loading