Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/janno/vmcast
  • ci/mtac2-tt
  • ci/ralf/atomic
  • ci/ralf/pm_red
  • ci/ralf/telescopes
  • ci/robbert/overloaded_wp
  • fast_string
  • gen_proofmode
  • iris-3.0
  • iris-3.1
  • janno/fix-566
  • janno/iframe-cbv
  • janno/iframe-no-upd
  • janno/ipm-strings
  • janno/ipm-strings-upstream
  • janno/metacoq
  • janno/try-HB
  • jh/done_contradiction
  • jh/evar_iframe
  • 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.019Apr1815141312111098730Mar292322212019181716151412111098765432129Feb28272625242322212019181716151413stroner atomic frame ruleOverload ⊥ in uPred_scope.Make levels of viewshifts consistent with implication/wand.Revert "Add the zero-width spaces at the *end* of the lines, and awe need 8.5pl1 nowMake compile with Coq 8.5pl1.Add the zero-width spaces at the *end* of the lines, and a newline before the first contextminor formatting nitsshuffle 0-width spaces around so they are distributed more evenlySmall tweak of spin lock.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqProof correctness of spin lock.Bool is inhabited.Make it compile with ssreflect masterignore more thingsUpdate README.Rename heap_lang/lib/heap.v -> heap_lang/heap.vBetter error message in case iRevert fails.Retry "Let iLöb automatically revert and introduce spatial hypotheses."Revert "Let iLöb automatically revert and introduce spatial hypotheses."Let iLöb automatically revert and introduce spatial hypotheses.Fix bug: iIntros "%" was doing the wrong thing.Use (more primitive) case instead of destruct in done tactic.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqIris Proofmode.Some properties about bigops on upred.Prove iff_equiv in the logic (instead of the model).Make pvs_wand_{l,r} consistent with pvs_impl_{l,r}.Remove wp_X> tactics and improve wp_finish.Remove unused lemmas wp_impl_{l,r}.Rename some old occurences of always stable into persistent.Make atomic a boolean predicate.Fix level of magic wand.Function to break a string up into words.Reimplement strip_later using type classes.forgot to add new file to _CoqProjectAdd a notion of a language based on evaluation context itemsCurried Permutation_cons instance.Add some comments explaining what these files doMisc language clean up.