theories/proofmode/environments.v · d7f8ff30c9285e4a2a60a4512104a5570a9e5084 · Lennard Gäher / Iris · GitLab

Find file Blame History Permalink

Turn the proof mode's `option_bind` into a definition. · d7f8ff30
Robbert Krebbers authored Nov 22, 2017
```
It used to be an inline pattern match.

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