diff --git a/Makefile.coq.local b/Makefile.coq.local
deleted file mode 100644
index b757c395c..000000000
--- a/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/Makefile.coq.local b/experimental_reals/Makefile.coq.local
deleted file mode 100644
index b757c395c..000000000
--- 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/discrete.v b/experimental_reals/discrete.v
index 63ca0e73b..412877a07 100644
--- a/experimental_reals/discrete.v
+++ b/experimental_reals/discrete.v
@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Corelib Require Setoid.
+From Coq Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect 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 b757c395c..000000000
--- 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/reals.v b/reals/reals.v
index 601ad4fe7..90bb30d87 100644
--- a/reals/reals.v
+++ b/reals/reals.v
@@ -38,7 +38,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-From Corelib Require Import Setoid.
+From Coq Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import boolp classical_sets set_interval.