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/algebra | |
| 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/algebra')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index e287c9e..fee34a2 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -977,7 +977,7 @@ Variable R : rcfType. Lemma poly_ivt : real_closed_axiom R. Proof. by case: R => ? []. Qed. Fact sqrtr_subproof (x : R) : - exists2 y, 0 <= y & if 0 <= x return bool then y ^+ 2 == x else y == 0. + exists2 y, 0 <= y & (if 0 <= x then y ^+ 2 == x else y == 0) : bool. Proof. case x_ge0: (0 <= x); last by exists 0; rewrite ?lerr. have le0x1: 0 <= x + 1 by rewrite -nnegrE rpredD ?rpred1. |