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.024Oct22212019181312111075432130Sep27262019181210331Aug3029241713112131Jul242319181713976543230Jun2928262523222120191817161514131211109876543131May302928272524232018171514111098743230Apr2928272625242322212019181211109654331Mar3028272422212019171615Tweak a proof.Proper pretty printing of new `|={E,E'}▷=>^n` notation.Merge branch 'joe/fupd_adequacy' into 'master'Use explicit names in some scripts, re-organize fupd plainly derived laws, adjust wsat import/export.Use plainly modality instead of typeclass in BiFUpdPlainly interface.Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd plainly interface and add new derived results.Coq 8.9 is no longer brokenMove `Atomic`, `IntoVal` and `AsVal` instances to lifting.ci/value_constr…ci/value_constructorAutomate proofs of `Atomic` instances.A specific constructor for injecting values in expressionsstart testing with Coq 8.9get rid of observations in ownP, they just make porting harderRemove spurious import.Replace more occurences of /\ by unicode ∧.Add type annotation.Use unicide ∧ and ∃.Add missing type in a signature.Bump Mtac2-8.8 commit.fix compatibility with Coq 8.7Merge branch 'ralf/prophecy' into 'master'Allow `IntoVal` to take pure steps.ci/robbert/into…ci/robbert/into_val_puresWeaken `PureExec φ n e1 e2` so that it can take `>= n` steps.Move `Atomic`, `IntoVal` and `AsVal` instances to lifting.Automate proofs of `Atomic` instances.Misc white space nits.Curry parA specific constructor for injecting values in expressionsnote some FIXMEsmore nitsuse 'proph' instead of a notation, and rename type of prophecy variables to proph_idmore nitsgeneralize to lists of observations per program stepfix nitsuse record for heap_lang stateMerge remote-tracking branch 'origin/master' into ralf/prophecy`(P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q)` holds for general BIs.Bump Mtac2-8.8 commit.Bump Mtac2-8.8 commit.Bump Mtac2-8.8 commit.fix typo