Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
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
Created with Raphaël 2.2.014Jun1312111098654131May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb27262524232221201918161514131298763231Jan2927252423222120191816131211107331Dec3029232221Change WP so that we have an fupd before the later, but after the quantification over next states.fix alignmentadd a test for framing monPred_at below a wandfix printing notation when importing heap_lang.lang after heap_lang.notationremove unnecessary importPlain typeclass should not require BiPlainly instance to be inferredfix format spacing for texan triplesMerge branch 'ralf/side-condition' into 'gen_proofmode'Fix issue #198.test via printing that the goal looks like it shouldalways split conjunctions in side-conditionsmake the way iMod solves side-conditions consistent with iInvMove bupd stuff from class_instances_sbi.v → class_instances_bi.v.class_instances: coqdoc; move higher priority instances up a bitMerge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmodemake emp_wand a LeftId instance, like True_implMove `into_forall_wand_pure` to the right file.fix 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_ne