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.05Oct4330Sep2618121031Aug2413112131Jul24231713976543230Jun29282625232221201918171615141312111098654131May30292825242320181715141198743227Apr26252423222120191811109654331Mar28272422212019161514131298765432128Feb27262524232221201918161514splitting up prophecy into separate fileSimpler proofFirst motivating example for prophecy variables (coin-flip)wp_fork changelogexplain RTLChangelog entry for !177.Merge branch 'robbert/cancelable' into 'master'`Cancelable` instances for gmap/option.ChangelogMerge branch 'ralf/curry-fork' into 'master'Merge branch 'ci/jh/r2l' into 'master'Right-to-left evaluation order.Merge branch 'robbert/strong_adequacy' into 'master'curry wp_forkfix clear pattern in destruct patternCoq master got 'better' at ltac backtraces, so we have to name some more functionsbump stdppStronger version of adequacy that also talks about state.Move `envs_incr_counter_equiv` to correct file, and state a corollary in terms of `of_envs`.use newer ocaml for Coq masterRemove `bi_hforall` and `bi_hexist`, these are superseded by the telescoped versions.use Docker image matching CI branchautoamtically use latest CIupdate CI for opam 2Fix confusing name of bound variable.Rename `prop_of_env` → `env_to_prop`Move theorems about `envs_` to `environments.v` where also these operations are defined.update CICoq 8.10 is broken for output as wellupdate a commentundo accidental editExport Ascii for compat with new Coqfix paradox pseudo-masksFix typo in the documentation. Thanks to Joe for pointing that out.Update lemma for frac_auth with fraction 1.CI issue was upstream in opam, partially revert the changesupdate CIupdate CIFix typo in comment.Clarify comment.