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.014Jun131211109876543131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar30282724222120191716151413121198765432128Feb272625242322212019181615141312987632Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmodedocument WP format stringsMerge branch 'ralf/reftests' into 'gen_proofmode'also test the output of error messagesMove local recursive ltac functions out to their own definitions to shorten backtracesbump stdppallow FrameMonPredAt to infer the indextrigger an anomaly in Coqralf/coqbug/iAc…ralf/coqbug/iAccu-anomalyMerge branch 'ci/ralf/monpred-frame' into 'gen_proofmode'make atomic_acc typeclasses-opaqueuse IntoVal for alloc specadd a tactic for the final introduction of an atomic accessorenable iMod to run an atomic updateadd a weak increment operation that knows it does not raceProve that atomic triples imply "normal" triplesAdd some lemmas about mapsto to the atomic_heap interfacemake atomic_heap a typeclass and add some notation for itUse telescopes for atomic accessors, updates and triples; add notation for all of themMerge branch 'gen_proofmode' into ci/ralf/telescopesforgot to update reference outputfix newlines being inserted in bad places for WPMerge branch 'gen_proofmode' into ci/ralf/telescopesfix yet another case of broken heap_lang notationmonpred test: use typed turnstile notationmonpred wand/impl framing: don't require indices to match syntacticallydifferent approach to monPred framingStop timing on Coq 8.7Fix inconsistent big operator instance names.Typo in CHANGELOG.mdMerge branch 'gen_proofmode' into ci/ralf/telescopesimprove printing of texan triplesMerge branch 'fupd_step_wp' into 'gen_proofmode'Update changlog.Mask-changing updates that take a step.Change WP so that we have an fupd before the later, but after the quantification over next states.fix alignmentadd a test for framing monPred_at below a wandfix printing notation when importing heap_lang.lang after heap_lang.notationremove unnecessary importPlain typeclass should not require BiPlainly instance to be inferred