heap_lang/substitution.v · 10e16fe0fd01f7503fc87bdbbed474bf55e5c2b6 · Janno / iris-coq · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

9 years ago
10e16fe0
Fallthrough instance for heap lang substitution. · 10e16fe0
Robbert Krebbers authored 9 years ago
```
Now we substitute as far into the term as we can. This is to deal
with terms that contain Coq variables.
```
10e16fe0

History
Fallthrough instance for heap lang substitution.
Robbert Krebbers authored 9 years ago
```
Now we substitute as far into the term as we can. This is to deal
with terms that contain Coq variables.
```