Add `head_prim_fill_reducible`. (!293) · Merge requests · Iris / Iris · GitLab

Snippets Groups Projects

Merged Dan Frumin requested to merge dfrumin/iris-coq:head_prim_fill_reducible into master 5 years ago

Jul 14, 2019
- Add `fill_prim_step` and `fill_reducible`. · 1357bde3
  Dan Frumin authored 5 years ago
  
  1357bde3
Jul 12, 2019
- Add `head_prim_fill_reducible`. · d479d17d
  Dan Frumin authored 5 years ago
  
  A more general implication from `head_reducible` to `reducible`.
  d479d17d