Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.024Oct222119181311754330Sep2618121031Aug2413112131Jul24231713976543230Jun29282625232221201918171615141312111098654131May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb2726252423222120Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd plainly interface and add new derived results.Coq 8.9 is no longer brokenstart 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.fix compatibility with Coq 8.7Merge branch 'ralf/prophecy' into 'master'note 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.fix typotest and support Coq 8.8.2Merge branch 'robbert/pure_exec_nsteps' into 'master'Add changelog entry for `PureExec`.Support multiple steps in `PureExec`.Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqUse only printing on notations for lambdas.heap_lang consistent spellingchangelogwhitespace tweaksdocument some heap_lang design choicestweak WP def.n and fix eauto in heap_langfix nitschange prophecy notationfix heap_lang/total_adequacyremove failing part of coin_flip; remove atomic_snapshotProving ownp.v and including it back into the buildfix TWPMaking prophecy-related examples work with the new prophecy supportAdding support for prophecy variables to heap_lang