From c0f6dcdb111e6b77c06678dd033a0239aa8e2891 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Wed, 24 Apr 2019 23:15:56 +0200
Subject: 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.
---
 mathcomp/algebra/ssrnum.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra')

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.
-- 
cgit v1.2.3