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/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
Created with Raphaël 2.2.023Feb22212019181716151413121110985432131Jan3029272625232221201918171614Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqchange ndot notation, againCancel a list of propositions.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqTurn stuff like iRes Definitions instead of Notations.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqnew notation for ndot, to avoid conflict with autosubstshow some dec_agree propertiesTweak decidable equality for language syntax....implement dec_agree (no lemmas about it yet)establish that language syntax has decidable equalityavoid a pitfall by not tying barrierG to heapG at allconsistently use the inG and inGF pattern for the barriertoday 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_canonical
Loading