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.025May2423222018161514131211875128Apr2625242322181615149876432131Mar272523212019181613121096428Feb2625242320191817151413121110765432130Jan292321181716151413111098720Dec19181413109654225Nov222120141312111087652131Oct2522181412119620Sep19131198630Aug2928272625242216141312Merge branch 'robbert/loeb' into 'master'Merge branch 'robbert/inv_combine' into 'master'CHANGELOG entry.Add lemma `inv_combine_dup_l`.Add lemma `inv_combine`.Rename `inv_sep` into `env_split`.Merge branch 'ci/ralf/dealloc' into 'master'Simplify proof of `tac_löb` using new lemma `löb_wand_intuitionistically`.Prove different versions of Löb rule.Name a variable in a `destruct`.Add lemma `intuitionistically_impl_wand_2 P Q : □ (P -∗ Q) ⊢ □ (P → Q)`.rename array_tools -> array; update CHANGELOGMerge branch 'robbert/cleanup' into 'master'Fine-grained split of `class_instances` based on the structure of the `bi` folder.Reorganize `big_op` file to remove `sbi` section.Reorganize `coq_tactics` file to remove `sbi` section.Rename `derived_laws_bi` → `derived_laws` and `derived_laws_sbi` → `derived_laws_later`.Merge branch 'ci/robbert/merge_sbi_new' into 'master'Merge branch 'robbert/done' into 'master'CHANGELOG entry.Comment for `internal_eq` file.Comment about `BiLaterMixin`.Explain axiom `⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q)` of embeddings.Add test file for a simple non step-indexed linear separation logic.Remove `Local` that is incompatible with Coq 8.9.Add smart constructor `BiMixin → BiLaterMixin`.Use type class for internal equality.Comment about `BiLöb`.Tweak error message and test case of `iLöb`.Add instances for Löb and contractiveness of later for monPred.Merge sbi canonical structure into the bi canonical structure.clarify commentMore documentation on `done`.test wp_freeapply review suggestionstest setoid_rewrite on inv_mapstomake inv_mapsto for heap_lang proper definitions because they are higher-orderMerge branch 'master' into 'master'Coqify the comments.Fix notation in comments