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/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/frame-frac
  • 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
  • ci/robbert/merge_sbi
  • ci/robbert/naive_solver
  • 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
34 results
Created with Raphaël 2.2.022Mar21201615141211109765124Feb2322212018171615141312111097632130Jan2928272625242322212017131211109876543128Dec2726232221201918161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817`FromAnd true` instances for big ops and ownership.Merge FromSep and FromAnd classes.No longer allow ownership of persistent elements to be split.Fix some typos in comments.work around Coq bug 5401 breaking 'Print HintDb typeclass_instances'Remove duplicate lemmas for agree.Some missing unicode arrows.Some simple lemmas for fractional.update std++Show an interesting lemma about the coreLet iAlways clear spatial context.Fix issue #80: better error message when hyps are missing.Remove old debugging code.Misc proof mode clean up.New internal IPM tactic: env_reflexivity.Remove Hint Mode that was already declared elsewhere (in classes.v).Support nat tokens in the tokenizer.Merge branch 'docs' into 'master' IntoModal --> FromModal in the docsUpdated the notation for lifting in ProofMode docsEnable solve_ndisj to solve `∅ ⊆ X`.Small tweaks.Fix possible divergence in framing.Better support for framing persistent hypotheses.make fractional lemmas use AsFractionalfix fractional IntoAnd instancesupdate stdppupdate coq-stdppBetter `iDestruct` support for big ops. This fixes issue #76.Later stripping under more connectives. This fixes issue #77.Oops, fix build.Mononicity of step taking fancy updates.proof tuningMisc properties about languages.Shorten a lemma.Merge branch 'fill_foldl'Define `fill` in terms of a `foldl` over `fill_item`.Merge branch 'more_spec_patterns'Update proof mode docs.More sane/consistent syntax for modal specialization patterns.