Merge pull request #68 from proux01/mc1343

Adapt to math-comp/math-comp#1343
math-comp · Feb 14, 2025 · c384ff4 · c384ff4
2 parents ea1d342 + 626505f
commit c384ff4
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 0 deletions.
diff --git a/theories/cauchyreals.v b/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.

diff --git a/theories/ordered_qelim.v b/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.

diff --git a/theories/qe_rcf.v b/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.

diff --git a/theories/qe_rcf_th.v b/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.