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.011Jan109876543128Dec2726232221201918161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817161514131210976543228Sep272120191514131298765432131Aug3029Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqRename tl_inG into na_inG.Merge branch 'coq-8.6' into 'master' Mark notation as "only printing"Use primitive projections for sealinguse coq 8.6 mode '!' to fix diverging apply:no longer test on or support Coq 8.5this is Iris 3.0.0!iris-3.0.0iris-3.0.0CHANGELOG: list things have been renamedMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqawk.Makefile: uninstall .v and .glob filesawk.Makefile: uninstall: also delete empty directoriesfix awk.Makefileupdate awk.Makefilelet solve_inG handle higher-arity functions for the \Sigmaadd a tactic to automatically solve goals that show inG from subGfix vio2vo patched targetMake instances EqDecision and Countable of gmultiset less eager.typomake Makefile work with POSIX awkpatch vio2vo target to only rebuild outdated .vo filesadd \Sigma for boxes; use a coercion for constant functorssimplify an inG proofdisable annoying warningMerge branch 'list_renaming_stuff'Recursive [inv_vec].Renaming in prelude/list.more restrictive Proof Using hints in (most files of the) preludemore restrictive Proof Using hints in base_logic, algebramore restrictive Proof Using hints in heap_lang, proofmode, testsfix CI testing for axioms in build outputprogram_logic: improve 'proof using' hint to be more minimal, more future-proofMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqAdd lemma compl_chain_map.a little theory about limit preservation"Proof using" hints for agree.vMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqdocument base_logic.upredtweak sigma COFEfix the build even more
Loading