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.030May2928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar30282724222120191716151413121198765432128Feb27262524232221201918161514131298763231Jan302927252423222120191816131211107331Dec30292322Fix 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.Mac's diff seems to be from the last century and can't do colors. Oh well.Use mktemp instead of tempfileupdate CIMerge branch 'master' into gen_proofmodebump std++; fix uses of defaultMerge branch 'master' into gen_proofmodeBump std++.Local update `(x, x) ~l~> (y, y)`.elim_inv_acc_with_close: also support ElimModal with a side-conditionprovide big_op lemmas outside of bi moduleMerge branch 'master' into gen_proofmodeA stronger version of `cinv_open`.don't export derived, that leads to uPred being the wrong moduleMerge remote-tracking branch 'origin/master' into gen_proofmodeRevert "Some results about `frac_auth` by Danny and Ales."Rename `cmra_opM_assoc` → `cmra_op_opM_assoc` and `cmra_opM_assoc'` → `cmra_opM_opM_assoc`.Stronger version of allocation rule for cancelable invariants.Merge branch 'ci/reftests' into 'gen_proofmode'Allow introduction patterns for result of `iCombine`.Move `Opaque iris_invG` to the appropriate place.Prove `□ False ⊣⊢ False`.don't check test output on coq.dev (it's broken due to a Coq bug)