Skip to content
Snippets Groups Projects
Select Git revision
  • Wclosed
  • atomic
  • big_op2_swap
  • big_sepL-inv
  • big_sepM2_lemmata
  • big_sepl_delete
  • bij
  • binder-insert
  • boxed
  • changelog_upd
  • ci
  • coq-8.6
  • dfrumin-master-patch-71378
  • docs
  • fill_reducible_no_obs
  • fresh_locs_arg
  • gmap_empty_included
  • gmultiset
  • is_closed_free_vars
  • isimpl_many
  • 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
28 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.02Mar129Feb282726252423222120191817161514131211109854321get rid of substitution in Case (use lambdas); introduce Match as derived form that involves bindersClean up anonymous binder hack.Use notation # instead of ' for literals to avoid conflicts.Generalize saved_props to any bifunctor.demonstrate a weird issueralf/magic-sing…ralf/magic-singletonWIP: nicer definition of head_stepMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqIntroduce cofeT -> cofeT functors, switch to bifunctors.WIP: expr as dependent typeforgot 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.