diff options
| author | Georges Gonthier | 2019-04-24 23:15:56 +0200 |
|---|---|---|
| committer | Georges Gonthier | 2019-04-24 23:15:56 +0200 |
| commit | c0f6dcdb111e6b77c06678dd033a0239aa8e2891 (patch) | |
| tree | d9547562b36ab587589c4daf0531e02ce5abc678 /mathcomp/field/separable.v | |
| parent | 5118bc30e1748dd58ddf30889c69502e9366f2d9 (diff) | |
remove deprecated use of `if ... return`
Replace improper use of non-dependent `return` clause in `if` with a
type cast; an upcoming coq-side PR will discontinue support for this,
in order to support dependent return clauses with an implicit `as`
annotation.
Diffstat (limited to 'mathcomp/field/separable.v')
0 files changed, 0 insertions, 0 deletions