Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/frame-frac
  • 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
  • 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
34 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.011Apr1098730Mar292322212019181716151412111098765432129Feb28272625242322212019181716151413Some 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.heao_lang/tactics: update some commentsDerive lifting axioms for ectx languagesdefine an interface of "evaluation-context-based languages" and use it for heap_langFinite powerset RA.Conversion gset -> gmap.Rename algebra/fin_maps.v -> algebra/gmap.vfix a typoMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: fix some comments raised by LarsMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqDisjointness of sets.update iris.styupdate namingMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqdocs: STS construction; explain why the RA core is not a homomorphismPreliminary list of naming conventions.update iris.styTODOMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqupdate bibMake use of COFE on lists in big ops.Add new algebra/list to _CoqProject.COFE structure on lists.More setoid properties of lists.Clean up algebra/option.