Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.010Oct975429Sep28272625242120191817161598628Aug2624232221201776428Jul14121027Jun13128625May1712927Apr261913121175431Mar302824232221201615141211109765124Feb2322212018171615141312111097632130Jan2928272625242322212017131211109876543128Dec2726232221201918161514131211987652130Nov2928272625Remove an unused argumentuse primitive projections for our mixinssync opam.pinsall opam caches are clear of the old pins by nowhave Coq's dev repos only for dev buildsupdate opam.pinsmore consistent grammarmake build-dep: prefer relative paths; they seem to work better on Windowsupdate std++; add test for solve_propertweak opam build-dep installationMerge branch 'hai/stdpp_update' into 'master'update stdppexplain make parallelismexplain updatingMake iInduction more powerful, to e.g. support well-founded induction.More consistent naming for `pure_exec`.Generalize `det_head_step_pureexec`.README: explain how to update std++Fix regression caused by e17ac4ad and another similar bug.fix build-dep on macOSFix `iIntros` regression caused by b0ae1102.Simplify solve_to_val.Fix issue #99.fix YAML even morefix YAMLCI tuningMerge branch 'pureexec' into 'master'add tests for recently fixed issuesMake `closed_dec` transparent by using `Defined`.Fix issue #97.Fix issue #98.update awk.MakefileMove some stuff.Get rid of `wp_done` and make more using of `IntoVal`.Let stateful tactics try all decompositions.Move out some PureExec assumptions into typeclassesReify expressions into values if `to_val e=Some v` is in the contextGet rid of the `pure.v` fileReorder the assumptions for `tac_wp_pure`Define PureExec for general language
Loading