Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/janno/strict-tc-resolution
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • ci/robbert/merge_sbi
  • ci/robbert/naive_solver
  • ci/robbert/set_unfold
  • ci/robbert/tc_opaque
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • 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
33 results
Created with Raphaël 2.2.019Apr1815141312111098730Mar292322212019181716151412111098765432129Feb282726252423222120191817161514Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqsome more playing around with the proof mode.Make iExact and iAssumption work under pvs and always.Misc clean up.tune proofs a littleshuffle 0-width spaces around so they are distributed more evenlyMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqRemove superfluous space in error of iPvs.Fix error handling of iApply.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqcopy Robbert's proof mode docMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqprove stronger frame-step for triplesBake a binder in the notation for the postcondition of wp and triples.stroner 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.