Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Lennard Gäher
Iris
Repository
8e455e525efb29b13b1f5e7f32c3e8809957989a
Switch branch/tag
iris
theories
heap_lang
proph_erasure.v
Find file
Blame
History
Permalink
Rename lemma `not_stuck_under_ectx` → `not_stuck_fill`, to be consistent with `stuck_fill`.
· 8e455e52
Robbert Krebbers
authored
Nov 25, 2019
Also refactor the proofs to make better reuse of existing lemmas.
8e455e52
