Fix import

analysis_stdlib/showcase/uniform_bigO.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
-From Coq Require Import Reals.
-From Coq Require Import ssreflect ssrfun ssrbool.
+From Stdlib Require Import Reals.
+From Corelib Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum.
 From mathcomp Require Import boolp reals Rstruct_topology ereal classical_sets.
 From mathcomp Require Import interval_inference topology normedtype landau.

experimental_reals/dedekind.v

@@ -8,7 +8,7 @@
 
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect_compat all_algebra.
-From Coq Require Import Setoid.
+From Corelib Require Import Setoid.
 
 (* -------------------------------------------------------------------- *)
 Set   Implicit Arguments.

experimental_reals/discrete.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Coq Require Setoid.
+From Corelib Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat all_algebra.
 From mathcomp.classical Require Import boolp.

reals_stdlib/Rstruct.v

@@ -1,7 +1,7 @@
 (* see below (after doc) for copyright notice *)
-From Coq Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
-From Coq Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
-From Coq Require Import Rtrigo1 Reals.
+From Stdlib Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
+From Stdlib Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
+From Stdlib Require Import Rtrigo1 Reals.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg poly ssrnum archimedean.
 

reals_stdlib/nsatz_realtype.v

@@ -1,4 +1,4 @@
-From Coq Require Import Nsatz.
+From Stdlib Require Import Nsatz.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrint ssrnum.
 From mathcomp Require Import boolp reals constructive_ereal.