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.014Sep1211108753230Aug29282412724Jul22211816151410432130Jun2926191817161513121187643130May29282726252423222018161514131211875129Apr28262524232219181615149876432131Mar272523212019181613121096428Feb262524232120191817151413121110765432130Jan292423211817161514131110Merge branch 'robbert/cmra_iso' into 'master'Apply 1 suggestion(s) to 1 file(s)Use validity restriction construction for auth.Isomorphism and validy restriction constructions for cameras.add missing changelog entryMerge branch 'ralf/to-agree-op-inv' into 'master'add a sed scriptfix '_L' suffixrename `agree_op_{inv,invL}'` to `to_agree_op_{inv,invL}`Misc trivial camera lemmas.Merge branch 'ralf/core-docs' into 'master'improve [core] docsimprove options-import checkonly check VFILES for options importClean up error handling code `iApply`.Merge branch 'ralf/functors' into 'master'add FunctorContractive instances, and also use this for auth and optionMerge branch 'ralf/options-file' into 'master'Merge branch 'ralf/internal-eq-entails' into 'master'fix a bunch of typos (thanks Tej)make sure we import 'options' everywhereadd internal_eq_entails uPred lawfix Proof Using warningsalso set Suggest Proof Usinguse options file everywhere that we so far set 'Proof using'add options file for library-wide configurationMerge branch 'document-makefile-options' into 'master'Merge branch 'better-makefile' into 'master'Use simple variables in MakefileDocument Makefile flags togetheradd some missing functorsdefine conversions between functorsAdd `cl_logic` folder to README.robbert/clproprobbert/clpropTests for `clProp` proof mode.Embedding `clProp` of classical logic into Coq.Add BI notation for negation.Prove that `BiPureForall` holds if we assume classical logic in Coq.Remove property `(∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝` from the BI canonical structure andAdd `si_logic` folder to README.Remove duplicate test of `test_iIntros_pure_not`.