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.08Oct765432130Sep29282726242322211615141211108753230Aug29282412724Jul22211816151410432130Jun2926191817161513121187643130May29282726252423222018161514131211875129Apr28262524232219181615149876432131Mar272523212019181613121096428Feb2625242321201918Merge branch 'robbert/counter' into 'master'Take comments into account.add IsOp instances for addition and min/maxgeneralize dfrac IsOp instanceMake the proof closer to the jungle proof.Cite jungle paper.Counterexamples for Affine+EM and Löb+EM.Merge branch 'robbert/view_auth_frac_rename' into 'master'Remove some redundant type annotations, which are not needed due to `Implicit Types`.Merge branch 'ralf/to-agree-op-valid' into 'master'add iff lemma for '✓ (to_agree a ⋅ to_agree b)'fix typo in MakefileCHANGELOG.Rename `auth_update_core_id` into `auth_update_frac_alloc`.Consistent 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.