Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.01Jun31May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb27262524232221201918161514131298763231Jan2927252423222120191816131211107331Dec3029232221201918151413121110Examples from MoSeL paper.Comments in tests/ipm_paper.improve README structureMerge branch 'master' into gen_proofmodeWhen framing, `▷ emp` should be turned into `emp` if the BI is affine.Typo typo.Fix typo in ProofMode.md (thanks to Hai).update Makefilemove 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'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`.