Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/3.1.0
  • ci/debug
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/stability
  • ci/value_constructor
  • fast_string
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • jh/evar_iframe
  • jh/independent_metric
  • jh/sprop_upred
  • jh_inductive_pairs
  • joe/bupd_derived
  • 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
30 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.04Jun3131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar30282724222120191716151413121198765432128Feb27262524232221201918161514131298763231Jan30292725242322212019181613rename atomic_step -> atomic_accprove lemmas to compose atomic stepsShow that atomic_step is an AccElim so we can open invariants; get entirely rid of the Em ⊆ Eo side-conditionadd iAuIntro tactic to prove an atomic update; introduce atomic_stepNew atomic updates: defined as a fixed point with existential quantifier; intro lemma using class of Laterable assertionsupdate CI and Makefileuse beq instead of Bool.eqb in envs_replaceci/ralf/pm_redci/ralf/pm_redadd an interesting test outputtests/ipm_paper: show goals where they were shown in the papertests/mosel_paper: show the two goals separatelyExamples from MoSeL paper.Comments in tests/ipm_paper.rename the proofmode copies to pm_option_bind and pm_default, respectively; move them to base and rename pm_red to reductionrename maybe_wand -> bi_wandMimprove README structureMerge branch 'master' into gen_proofmodeWhen framing, `▷ emp` should be turned into `emp` if the BI is affine.Typo typo.bump Mtac commitmoved of_expr to M because it made code simpleradapting to reflexivity as ttacadapting to reflexivity as ttacFix typo in ProofMode.md (thanks to Hai).update Makefilemake maybe_wand a BI connective; simplify BI connectives in proof modeinstead of maybe_wand_sound, let the proofmode support maybe_wandMore reduction controlmove the reduction control of the proofmode to its own file and tweak itmove comment closer to where it is exploitedbump std++, use the new [default] notationremove bi.big_... compatibility aliases for big-opsMerge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmodeFix iInv for monpred and test thatBetter `IntoWand` instances for `<affine> ⎡ ... ⎤` as an alternative for ec4ac846.Stronger `IntoWand` instance for the □ modality.`IntoWand` instances for the affine modality.Revert `IntoWand` part of ec4ac846, and associated change in 9b14f90a.fix into_wand for monpred proofmodeMerge branch 'ralf/bigop' into 'gen_proofmode'Bump Mtac2 commit.