Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • 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
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.023Feb22212019181716151413121110985432131Jan3029272625232221201918171614131298today is not my day...hopefully really fix build *oops*more cancelling in barrierheap_lang: try to use cancelsts, auth: use cancelfix the buildbarrier: strive for consistency between barrierGF and the inGF assumptions; also change some instance namesRevert "turn canonical structures that don't have any instances into plain records"turn canonical structures that don't have any instances into plain recordsA very simple separation logic canceler by reflection.Move global functor construction to its own file and define notations.Move global functor construction to its own file and define notations.Restraint instance search for global functors.Remove obsolute FIXME.Fix notation for ndot.Fix mess by my previous commits ...Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqLet set_solver not use eauto by default.Let set_solver not use eauto by default.Small STS tweaks.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqMake naive_solver a bit more robust.hide which exact functors the barrier needsadd notation for ndotadd the infrastructure for Coq to automatically infer the "inG" instancesFAIL : Less canonical projections.less_canonicalless_canonicalCI: parallel buildtry to tell gitlab CI what to doprovide a closed proof of the clientmake fn_cons universe polymorphic... otherwise, I run into universe errors :-/move a TODO aroundadd a notion of cons-ing a funcion, and notation for itMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqUse ewp tactic in heap_lang/tests.Simplify some heap_lang proofs.Some uPred style consistency tweaks.Change order or later and always so that the Löb lemmas are grouped.add a (dummy) clienthide disjointness better from the clientprove pvs_sep
Loading