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.010Jun98654131May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb27262524232221201918161514131298763231Jan2927252423222120191816131211107331Dec3029232221201918fix iSpecialize on pure assertionsbump std++Merge branch 'ralf/into_forall_wand' into 'gen_proofmode'allow specializing a wand with a Coq-level proof of the premiseMerge branch 'ralf/tc_control_full' into 'gen_proofmode'Merge branch 'master' into gen_proofmodefix markdownconvert Naming to markdownimprove naming convention doc for sufficesMerge branch 'master' into 'master'Added naming conventions for definitions to naming.txtalso use iSolveTC for heap_langconsistently use iSolveTC to solve typeclass goalsmake updates and magic wand linebreaks consistent with coq built-in notationturns out we don't need the hv in any of thisfix linebreak behavior for binary update modalitiesmove printing-only tests to their own sectionstest how WP prints when the code gets longimprove linebreak tests so that they do not rely on infix renderingtest proofmode output for long lines, and fix itremove an unused importMerge branch 'ralf/upred' into 'gen_proofmode're-state and not just register ownM_ne, cmra_valid_nemove uPred-specific proofmode integration into its own filemove re-wrapping of iris-specific lemmas to bi.vbe more explicit about instance scope; move Hint to the lemma it usesuse unicodereserve embedding notation as wellalso reserve monPred modalitiesalso pre-reserve bigops notationreserve fancy update notationMake uPred itself independent of BI interface and just prove primitive laws (like in master branch)remove legacy hint db entriesremove base_logic/deprecatedactually the LHS of [of_envs] is persistent AND affineadd an interesting test outputrename atomic_step -> atomic_accprove lemmas to compose atomic stepsShow that atomic_step is an AccElim so we can open invariants; get entirely rid of the Em ⊆ Eo side-conditionadd iAuIntro tactic to prove an atomic update; introduce atomic_step