Skip to content
Snippets Groups Projects
Select Git revision
  • atomic
  • ci/3.1.0
  • ci/debug
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/stability
  • ci/value_constructor
  • fast_string
  • iris-3.0
  • iris-3.1
  • janno/metacoq
  • jh/done_contradiction
  • jh/evar_iframe
  • jh/independent_metric
  • jh/sprop_upred
  • jh_inductive_pairs
  • joe/bupd_derived
  • 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
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.016Mar15141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec272623222120191817161514131211987652130Nov2928272625242322212019181716151098765432131Oct302827262522211817Fix 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.Extend specialization patterns.CI config: run CI on all branches starting with 'CI'some more STS lemmasalso add my original testcase, just to be sureUpdate to latest stdpp.Fix issue #74.make frac_included into general lemma about < and + of positive fractionsrename wp_fupd_step -> wp_step_fupd. All other lemmas call them step_fupd.show some more local updates for the option typeadd test for iNext with evarsMake IntoLaterN work on ▷ ?P with ?P an evar.