theories/proofmode/base.v · d7f8ff30c9285e4a2a60a4512104a5570a9e5084 · Gaëtan Gilbert / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

7 years ago
d7f8ff30
Turn the proof mode's `option_bind` into a definition. · d7f8ff30
Robbert Krebbers authored 7 years ago
```
It used to be an inline pattern match.

This also restores compatibility with Coq 8.6.1.
```
d7f8ff30

History
Turn the proof mode's `option_bind` into a definition.
Robbert Krebbers authored 7 years ago
```
It used to be an inline pattern match.

This also restores compatibility with Coq 8.6.1.
```