Adapt to https://github.com/math-comp/math-comp/pull/1343

theories/cauchyreals.v

@@ -1,5 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
+From Coq Require Setoid.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import fintype bigop binomial order perm ssralg poly.
 From mathcomp Require Import polydiv ssrnum ssrint rat matrix mxpoly polyXY.
@@ -561,7 +562,7 @@
 Proof. by case: x. Qed.
 
 Definition cauchymod :=
   nosimpl (fun (x : creal) => let: CReal _ m := x in projT1 m).
 
 Lemma cauchymodP (x : creal) eps i j : 0 < eps ->
   (cauchymod x eps <= i)%N -> (cauchymod x eps <= j)%N -> `|x i - x j| < eps.
@@ -884,7 +885,7 @@
 Qed.
 
 Definition ubound (x : creal) := 
   nosimpl (let: exist2 b _ _ := ubound_subproof x in b).
 
 Lemma uboundP (x : creal) i : `|x i| <= ubound x.
 Proof. by rewrite /ubound; case: ubound_subproof. Qed.

theories/ordered_qelim.v

@@ -1,5 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
+From Coq Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
 From mathcomp Require Import choice fintype bigop finset order fingroup.

theories/qe_rcf.v

@@ -1,5 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
+From Coq Require Import Setoid.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import div choice fintype finfun bigop order ssralg zmodp.
 From mathcomp Require Import poly polydiv ssrnum ssrint interval matrix polyXY.

theories/qe_rcf_th.v

@@ -1,5 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
+From Coq Require Import Setoid.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp Require Import polyorder polyrcf mxtens.