Skip to content
Snippets Groups Projects
Select Git revision
  • core
  • master default protected
  • new_master
  • simon/parametric-index
  • step-index-class
5 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.016Jun1514131211109765432131May3029282625242321201916151312987642130Apr292726252423178729Mar26222019171615141376543128Feb27262524232221201816137653130Jan29282726252423221918171514131110225Dec22212019181514131210876330Nov292827262220161211986131Oct2927262524222119181311754330Sep2618121031Aug242131Jul24231713976543230Jun29282625232221201918Merge branch 'fix-iEval-precedence' into 'master'Comment about the relation between `discrete_fun` and non-expansive functions.Update `StyleGuide.md`.Replace `C`s with `O`s since we use OFEs instead of COFEs.Merge branch 'offset_lifting' into 'master'Add lifting lemmas for operations under offset (list and vector versions).Fix overloaded notation behaviour for offset addition.Use consistent meta variables for `wp_invariance`.Bump std++.tactic->tactic3 for remaining tacticstactic->tactic3 for user-facing tacticsFix inconsistent invocation of iPoseProofCoreLemFix parsing precedence for iEvalcomparison: treat prophecies like unitmake variable names a bit more consistent between Coq and LaTeXcentralize all heap_lang notation in one fileMerge branch 'lazy_coin' into 'master'Add the lazy_coin exampleMerge branch 'ralf/adequacy' into 'master'avoid some evarstweak adequacy: treat stuckness like the other WP indices`IntoSep` instance for `tc_opaque`.Coqdoc tweaks.Add lemma `meta_token_difference`.Merge branch 'robbert/adequacy' into 'master'move comments out-of-line to please the extremely picky macOS shelltry to fix test suite for macOSnote on macOS sed usagestate adequacy helper lemma more positivelyupdate docs for new adequacy statementRemove useless import.Tweak the proof of `wp_adequacy`.CHANGELOG entry.Comment about traces.A strong adequacy statement to rule them all.add sed script for frac_auth changeswith reftest normalization, whitelisting Coq 8.11 should not be needed any moreMerge branch 'ralf/frac_auth' into 'master'change frac_auth notationFix compilation with Coq master.