Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/janno/debug-opam
  • ci/janno/let_bind_envs
  • ci/janno/vmcast
  • ci/joe/compact_ipm
  • ci/joe/compact_ipm_remaining
  • ci/joe/compact_ipm_simple
  • ci/msammler/iris-coq-seal_big_opM
  • ci/ralf/pm_red
  • ci/ralf/retime
  • ci/ralf/set_unfold_elements
  • ci/ralf/transfinite
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/naive_solver
  • ci/robbert/set_unfold
  • iris-3.2.0
  • 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
31 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.017Sep1615141198628Aug2624232221201776428Jul14121027Jun13128625May1712927Apr261913121175431Mar302824232221201615141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec272623222120191817161514131211987652130Nov292827262524232221Update to latest stdpp, and set Hint Mode of classes.fix CIMerge branch 'master' into 'master'Add examples of IPM paper to tests/ipm_paper.v.WIPa few more tacticsfinished reshape_expr', although I have no idea if what I'm doing is what is intendedstill working on heap_lang/tacticsusing match_goal context to perform substitutionAdded evar for typeclass resolutionusing new notation for list of tacticsremoving type-in-type and making it work with the new versionAnd another universe inconsistency, even with type-in-type...Use -type-in-type and bump stdpp.MetaCoq hacking.Add notes.Stuff.Set notation scopes of some language stuff.Printing boxes and breaking points for WP.Some notation tweaking.Bump coq-std++.Bump coq-stdpp.More consistent behavior of `#H` when the source is already in theOptimize wp_apply and improve its error reporting.Fix error reporting of iSpecialize.Small optimization for iSpecialize.Update lock.vMore consistent naming for fixpoints.Make it possible to introduce □ ⌜ φ ⌝ as a pure hypothesis.Merge branch 'ralf/greatest-fix' into 'master'no more wandmove quantifiersMerge remote-tracking branch 'origin/master' into ralf/greatest-fixreorder induction principleFix spurious whitespaceFix issue #95.also do least fixpoint; fix namingMerge branch 'refactor-ticket-lock' into 'master'Implement greatest fixed point inside the logicupdate regexp for coq 8.7
Loading