Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.06Oct5432130Sep29282726242322211615141211108753230Aug29282412724Jul22211816151410432130Jun2926191817161513121187643130May29282726252423222018161514131211875129Apr28262524232219181615149876432131Mar272523212019181613121096428Feb2625242321201918171514Consistent naming for auth/view lemmas.update build systembetter way to trigger TC searchMerge branch 'ralf/dfrac' into 'master'exploit irreflexivityMerge branch 'robbert/hide_ipreprop' into 'master'dfrac: do not track discarded fractionMake everything related to `inG_fold`/`inG_unfold`/`iRes_singleton` local.CHANGELOG.Factor out `inG_unfold_validN`.Put isomorphism `iProp` to `iPreProp` into `own` construction.Add `valid_entails` to lift `✓{n}` entailments into `uPred`.Add lemmas for updates on isomorphic cameras.Add lemma `cmra_transport_trans`.Merge branch 'robbert/cmra_morphism_valid' into 'master'CHANGELOG.Rename `cmra_monotone_valid` into `cmra_morphism_valid`.`Set Default Proof Using` is not needed due to `options`.Merge branch 'discardable-fractions' into 'master'Add dfracMerge branch 'ralf/auth-changelog' into 'master'expand auth changelogBump stdpp.Bump std++.Merge branch 'ci/robbert/view' into 'master'CHANGELOG.Remove lemma `view_equivI` and document that.Add documentation for auth & view.Add `included_both` lemmas for auth & view.Add injectivity instances for `●` and `◯` for auth & view.Add lemma `view_update_frag`.Generalize inclusion lemmas for view & auth to iff.Add inclusion lemmas for view & auth.The view camera and redefine the auth camera in turns of it.Merge branch 'robbert/bi_pure_forall' into 'master'More Coqdoc.Remove ¬ notation in counterexamples.ASCII notation for negation in bi_scope.Merge branch 'msammler/multithread_adequacy' into 'master'CHANGELOG.