Remove Stdlib dependency

Makefile.coq.local

@@ -0,0 +1,8 @@
+pre-all::
+	if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
+	  for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \
+	     sed -i.bak $${f} -e 's/From Corelib/From Coq/' ; \
+	     sed -i.bak $${f} -e 's/PosDef/PArith/' ; \
+	     $(RM) $${f}.bak ; \
+	  done ; \
+	fi

theories/proof/Makefile.coq.local

@@ -0,0 +1,8 @@
+pre-all::
+	if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
+	  for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \
+	     sed -i.bak $${f} -e 's/From Corelib/From Coq/' ; \
+	     sed -i.bak $${f} -e 's/PosDef/PArith/' ; \
+	     $(RM) $${f}.bak ; \
+	  done ; \
+	fi

theories/proof/approx.v

@@ -1,11 +1,11 @@
 (* (c) Copyright 2006-2018 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
+From Corelib Require Import Setoid Morphisms.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import fintype tuple path fingraph bigop order ssralg.
 From mathcomp Require Import ssrnum ssrint div intdiv.
 From fourcolor Require Import hypermap geometry coloring grid matte.
 From fourcolor Require Import real realplane.
-From Coq Require Import Setoid Morphisms.
 From fourcolor Require Import realsyntax realprop.
 
 (******************************************************************************)

theories/proof/dedekind.v

@@ -1,9 +1,9 @@
 (* (c) Copyright 2006-2018 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
+From Corelib Require Import Setoid Morphisms.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq order.
 From mathcomp Require Import ssralg ssrnum ssrint rat.
 From fourcolor Require Import real.
-From Coq Require Import Setoid Morphisms.
 
 (******************************************************************************)
 (*   Construcion of the real numbers as a complete totally ordered field.     *)

theories/reals/Makefile.coq.local

@@ -0,0 +1,8 @@
+pre-all::
+	if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
+	  for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \
+	     sed -i.bak $${f} -e 's/From Corelib/From Coq/' ; \
+	     sed -i.bak $${f} -e 's/PosDef/PArith/' ; \
+	     $(RM) $${f}.bak ; \
+	  done ; \
+	fi

theories/reals/realcategorical.v

@@ -1,8 +1,8 @@
 (* (c) Copyright 2006-2018 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
+From Corelib Require Import Setoid Morphisms.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq order.
 From mathcomp Require Import ssralg ssrnum ssrint rat.
-From Coq Require Import Morphisms Setoid.
 From fourcolor Require Import real realsyntax realprop.
 
 (******************************************************************************)

theories/reals/realprop.v

@@ -1,8 +1,8 @@
 (* (c) Copyright 2006-2018 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
+From Corelib Require Import Morphisms Setoid.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div order.
 From mathcomp Require Import ssralg ssrnum ssrint archimedean rat intdiv.
-From Coq Require Import Morphisms Setoid.
 From fourcolor Require Import real realsyntax.
 
 (******************************************************************************)