Skip to content
Snippets Groups Projects
Select Git revision
  • ascii-sections
  • basic-dune
  • bi_pure_scopes
  • doc-equalities
  • explicit-vdash
  • fix-497-hint-immediate
  • fix-notation
  • fupd-commutes
  • inv_exc_0_ipm
  • later-credits-drop
  • later_impl_experiments
  • later_impl_test
  • master default
  • more-convenient-fupd_proper
  • no-bi-canonical
  • notations
  • paolo/tc-strict-resolution-backport
  • periscopes
  • periscopes-v2
  • seal_ires
  • iris-4.3.0
  • iris-4.2.0
  • iris-4.1.0
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • 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
39 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.024May2320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb27262524232221201918161514131298763231Jan2927252423222120191816131211107331Dec302923222120191815141312111087Merge 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)clean up test tmpfile; remove .vo if test failed so it gets re-runfix test suite makefile to work with Coq mastermake clean should clean the tests directory if it existsmove test suite out of theories/ so it does not get installed; also check output of test suite so that we can test printingMerge branch 'master' into gen_proofmodeMove generic `IsOp` instances to `algebra/proofmode_classes.v`.`IsOp` instance for singleton map.Rename `frag_auth_op` into `frac_auth_frag_op` (the old name was inconsistent).Merge branch 'ralf/inv' into 'gen_proofmode'Fix typo.False is affine.Merge branch 'master' into gen_proofmodeBump std++.use m as prefix for things of option typemake a proofmode copy of from_option to control simplificationMerge branch 'master' into 'master'All multiset elements are cancelable.Some results about `frac_auth` by Danny and Ales.Misc monPred tweaks.update CI/Makefilefix make build-dep