diff --git a/analysis_stdlib/showcase/uniform_bigO.v b/analysis_stdlib/showcase/uniform_bigO.v
index 4b1afb63c4..1b87137a4e 100644
--- a/analysis_stdlib/showcase/uniform_bigO.v
+++ b/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.
diff --git a/experimental_reals/Makefile.coq.local b/experimental_reals/Makefile.coq.local
deleted file mode 100644
index b757c395c1..0000000000
--- a/experimental_reals/Makefile.coq.local
+++ /dev/null
@@ -1,8 +0,0 @@
-pre-all::
-	if command -v coqc > /dev/null && (coqc --version | grep -q '8.20') ; then \
-	  for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \
-	     sed -i.bak 's/From Corelib/From Coq/' $${f} ; \
-	     sed -i.bak 's/PosDef/PArith/' $${f} ; \
-	     $(RM) $${f}.bak ; \
-	  done ; \
-	fi
diff --git a/experimental_reals/dedekind.v b/experimental_reals/dedekind.v
index fa11b8c223..f23f34b7b4 100644
--- a/experimental_reals/dedekind.v
+++ b/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.
diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v
index 0126103880..1d9780925a 100644
--- a/experimental_reals/discrete.v
+++ b/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.
diff --git a/reals/Makefile.coq.local b/reals/Makefile.coq.local
deleted file mode 100644
index b757c395c1..0000000000
--- a/reals/Makefile.coq.local
+++ /dev/null
@@ -1,8 +0,0 @@
-pre-all::
-	if command -v coqc > /dev/null && (coqc --version | grep -q '8.20') ; then \
-	  for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \
-	     sed -i.bak 's/From Corelib/From Coq/' $${f} ; \
-	     sed -i.bak 's/PosDef/PArith/' $${f} ; \
-	     $(RM) $${f}.bak ; \
-	  done ; \
-	fi
diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v
index 5ef445a76f..4d062072b8 100644
--- a/reals_stdlib/Rstruct.v
+++ b/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.
 
diff --git a/reals_stdlib/nsatz_realtype.v b/reals_stdlib/nsatz_realtype.v
index dfff679cf4..bcb6561cd0 100644
--- a/reals_stdlib/nsatz_realtype.v
+++ b/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.