Skip to content
Snippets Groups Projects
Select Git revision
  • ci/3.1.0
  • ci/debug
  • ci/disable-ltac-backtrace
  • ci/for_proph
  • ci/janno/debug-opam
  • ci/janno/let_bind_envs
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/joe/compact_ipm_remaining
  • ci/joe/compact_ipm_simple
  • ci/maximedenes/instance-nobody-open-proof
  • ci/msammler/iris-coq-seal_big_opM
  • ci/mtac2-tt
  • ci/prophecy
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/ralf/set_unfold_elements
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • 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
31 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.011Apr109654331Mar30282724222120191716151413121198765432128Feb27262524232221201918161514131298763231Jan302927252423222120191816131211107331Dec302923222120191815141312111087654gmultiset RABump the std++ versionupdate CIBump std++.Merge branch 'robbert/embed_emp' into 'gen_proofmode'only run coqchk in one jobbump std++rename : affinely_persistently -> intuitionistically. Add lemma about monpred_at and intuitionistically.ofe_funC_ofe_discrete and ofe_funR_cmra_discrete.update CImove OPAM_PKG to the 8.8+beta1 job as that one is spawned firstalso time against Coq 8.8 betaupdate std++ to make sure we have all notations aroundMerge branch 'ralf/bi_disambig' into 'gen_proofmode'fix notation conflictmake the annotated notations only parsing; add annotated versions of the curried forms (⊢) and (⊣⊢)dont print curl invocationsubmit timingbenchmark against 8.7.1 (same as iris-3.1)add '@' to type ascription notation for disambiguationadd notation to define the PROP we use for a particular turnstileMerge branch 'robbert/ElimModal' into 'gen_proofmode'Separate type class for `■ ⎡P⎤ ⊢ ⎡■ P⎤`.Remove embed emp axiom.Document `ElimModal`.Extend ElimModal with Boolean flags to specify whether it operates on the persistent/spatial context.Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmodeMerge branch 'master' into gen_proofmodeupdate CIFix some bad names.Slightly more easy to use version of strong `inv_open`.clean up CI for this special case, this is non-master anywayfix CPU_CORESpropery disable 8.6.1, and test 8.7.2 instead of the moving 8.7.devStronger version of `inv_open` that allows to close invariants in a different order.update CIMerge branch 'ralf/lemma_rename' into 'gen_proofmode'fix gitlab-extract output if build is still runningupdate CIstop adding the quick2vo target