Skip to content
Snippets Groups Projects
Select Git revision
  • adjust-focused-goal
  • atomic
  • avoid-deprecated-arith
  • byte-strings
  • bytes-ident
  • 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
  • cmra-iso
  • cmra-restrict-valid
  • coqide-unicode-config
  • dfrac-smart-constructor
  • dfrac-valid-arg
  • document-ipm-classes
  • 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.019Sep18171615141198628Aug262423222120181776428Jul14121027Jun13128625May1712927Apr261913121175431Mar302824232221201615141211109765124Feb23222120181716151413121110987632130Jan2928272625242322212017131211109876543128Dec272623222120191817161514131211987652130Nov2928272625242322Use a type class for monotone uPred predicates.Show that heap_lang expressions are countable.CI: depend on std++ via opam; prepare for automatic opam releasesGet rid of TimelessL and PersistentL and use TCForall instead.Use ε for CMRA unit.Fix previous commit.Update to latest stdpp, and set Hint Mode of classes.fix CIiris-3.0iris-3.0Merge 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.Adding telescopes and some useful lemmas.telescopetelescopeUpdate 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-fix