Skip to content
Snippets Groups Projects
Select Git revision
  • 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
  • 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.
Created with Raphaël 2.2.01Mar29Feb28272625242322212019181716151413121110985432131Janforgot to ammend this...fix name of recv_strengthen to recv_weakenLoad should bind more strongly than app.Use "R"-suffixes for CMRA instances.strengthen recv_split: no more skipdocs: tying the list of authors to one of the iris papers is rather sillyfix the docsprove "THE CLIENT"prove a weaker derived form of recv_strengthen; more "\lam:" notationrename: minus -> div. Also change notation accordingly.simplify cauchy condition on chainspreparations for describing agreement in The Iris Documentationcomplete description of COFEswordingmove some explanations from iris 2.0 paper to heresome tex nitsnewchan -> newbarrierReplace occurences of -> by →.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqNotation for Case that is consistent with the constructor names.make auth_fsa consistent about const-valid vs uPred-validprove a lemma for splitting \mapstobe 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.