diff options
| author | Georges Gonthier | 2019-04-25 00:40:16 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-25 00:40:16 +0200 |
| commit | dec1f90d13c44016ea53da360e9692fd768bc24b (patch) | |
| tree | d9547562b36ab587589c4daf0531e02ce5abc678 | |
| parent | 5118bc30e1748dd58ddf30889c69502e9366f2d9 (diff) | |
| parent | c0f6dcdb111e6b77c06678dd033a0239aa8e2891 (diff) | |
Merge pull request #335 from math-comp/fix-if-return
remove deprecated use of `if ... return`
| -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. |