Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • atomic
  • ci/janno/vmcast
  • ci/ralf/atomic
  • ci/ralf/mtac2-tt
  • ci/ralf/pm_red
  • ci/ralf/telescopes
  • ci/robbert/overloaded_wp
  • fast_string
  • gen_proofmode
  • ipm-notation-broken
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/affine_frompure
  • jh/done_contradiction
  • jh/evar_iframe
  • jh/independent_metric
  • jh/move_bi_affine
  • jh/sprop_upred
  • jh_inductive_pairs
  • 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
30 results
Created with Raphaël 2.2.030Jul8Jun76543131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar30282724222120191716151413121198765432128Feb27262524232221201918161514131298763231Jan3029272524NEW: Now with strange typing error.mastermasterfix markdownconvert Naming to markdownimprove naming convention doc for sufficesMerge branch 'master' into 'master'Added naming conventions for definitions to naming.txtMerge remote-tracking branch 'origin/gen_proofmode' into ci/ralf/telescopesci/ralf/telesco…ci/ralf/telescopesadd general telescopes and telescopic BI binders and proofmode supportalso use iSolveTC for heap_langralf/tc_control…ralf/tc_control_fullconsistently use iSolveTC to solve typeclass goalsmake atomic_heap a typeclass and add some notation for itci/ralf/atomicci/ralf/atomicnote two TODOsBump Mtac commit.mtac2-ttmtac2-ttFormat specifier for atomic triple and update notation; also change update notationUse telescopes for atomic accessors, updates and triplesadd general telescopes and telescopic BI binders and proofmode supportuse beq instead of Bool.eqb in envs_replacerename the proofmode copies to pm_option_bind and pm_default, respectively; move them to base and rename pm_red to reductionmake maybe_wand a BI connective called bi_wandM; simplify BI connectives in proof mode using cbnmove the reduction control of the proofmode to its own file and tweak itmake updates and magic wand linebreaks consistent with coq built-in notationgen_proofmodegen_proofmodeturns out we don't need the hv in any of thisfix linebreak behavior for binary update modalitiesmove printing-only tests to their own sectionsUse "match … exhaustively_with" in `W.of_expr`.test how WP prints when the code gets longimprove linebreak tests so that they do not rely on infix renderinguse beq instead of Bool.eqb in envs_replaceralf/pm_redralf/pm_redrename the proofmode copies to pm_option_bind and pm_default, respectively; move them to base and rename pm_red to reductionmake maybe_wand a BI connective called bi_wandM; simplify BI connectives in proof mode using cbnmove the reduction control of the proofmode to its own file and tweak ittest 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 well