Skip to content
Snippets Groups Projects
Select Git revision
  • arrays
  • atomic
  • atomic_resolve_alternative
  • cas_resolve
  • ci/3.1.0
  • ci/debug
  • ci/disable-ltac-backtrace
  • ci/janno/debug-opam
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/maximedenes/instance-nobody-open-proof
  • ci/prophecy
  • ci/ralf/ci
  • ci/ralf/pm_red
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/tc_opaque
  • ci/stability
  • ci/value_constructor
  • fast_string
  • 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.027Apr2625242322212019181211109654331Mar30282724222120191716151413121198765432128Feb27262524232221201918161514131298763231Jan302927252423222120191816131211107331Dec3029232221201918151413121110Bump Mtac commit. [Still on temporary branch.]Bump Mtac commit. [Still on temporary branch.]Bump std++.Fix #184.Bump Mtac commit. [Still on temporary branch.]Bump Mtac commit. [Still on temporary branch.]I think I made the previous commit in the wrong project... anyway, bump std++bump IrisBump Mtac version. [Still on temp. branch.]Temporarily use non-master branch of Mtac2.have two instances for ElimInv and MakeEmbed, instead of one horrible oneBump Mtac version.New IntoAcc typeclass to decouple creating and elliminating accessors; ElimInv supports both with and without Hcloserename InvOpener -> AccElimaccessor-style iInv without HcloseMerge remote-tracking branch 'origin/master' into gen_proofmodeupdate MakefileUse new `[!APP]` branches wherever it makes sense.Merge branch 'ralf/ipm-bootstrap' into 'gen_proofmode'fix Makefileonly do the 'reinstall build-dep package' on opam 1update CICI: let's see if opam reinstall works faster than opam upgrade for changing build-depsuse Lemma, not Letimprove wp_apply evar testadd test for wp_apply and evars (#181)enable a test that failed with Coq 8.6proofmode: make it possible for class_instances to use the proofmodeMerge branch 'robbert/done_evar' into 'gen_proofmode'bump std++actually solve_proper can do thisstrengthen fixpoint non-expansiveness lemmasLet `done` and friends fail when the proofmode goal is an evar. Fix issue #181: let `wp_expr_eval` check that the goal is in fact a WP.Bump Mtac2 commit.when the goal is an evar, pick emp when possibleralf/emp-introralf/emp-intromake fixpoints simpl nevermore mask-related fancy update lemmasprove generally applicable lemmas for non-mask-matching fancy updatesupdate CI
Loading