Skip to content
Snippets Groups Projects
Select Git revision
  • polymorphic-bi
  • master default protected
  • fix-doc-links
  • parametric-algebra
  • fix-proof-coq-master
  • dfrac-valid-arg
  • avoid-deprecated-arith
  • adjust-focused-goal
  • prefix-automatic-names
  • qualify-instances
  • exists-intro-pattern
  • document-ipm-classes
  • fix-intuitionistic-spatial
  • strong-frag-validity/view-bij
  • dfrac-smart-constructor
  • rauth
  • cmra-restrict-valid
  • cmra-iso
  • port-auth_map
  • efficient-heaplang-tactics
  • 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
Compare
Forked from Iris / Iris
Source project has a limited visibility.
user avatar
Prove fixpointK stuff without unfolding the definition of fixpoint.
Robbert Krebbers authored 
Also, give names to hypotheses that we refer to.
1b4ded4d
History
user avatar 1b4ded4d
History
Name Last commit Last update