diff options
| author | Georges Gonthier | 2019-03-18 12:49:18 +0100 |
|---|---|---|
| committer | Georges Gonthier | 2019-03-18 12:49:18 +0100 |
| commit | 7f25b156d2e33ec767732175f7030cd103e9b695 (patch) | |
| tree | 94eddb7e9bca379c3ec50e73c91301da459a0d18 /mathcomp/Make | |
| parent | e6622f6910759ed8bf07ce94827da778d397d228 (diff) | |
remove dependency on hidden case branch types
Anticipating coq/coq#9170, remove numeric occurrence selector affected
by the (invisible) presence of explicit types for variables bound in
`match` branch patterns. The proof could be further simplified if this
change is implemented.
Diffstat (limited to 'mathcomp/Make')
0 files changed, 0 insertions, 0 deletions