Merge pull request #97 from proux01/no-stdlib

Remove Stdlib dependency

.github/workflows/ci.yml

@@ -8,26 +8,16 @@ jobs:
     strategy:
       matrix:
         image:
-          - mathcomp/mathcomp:2.0.0-coq-8.16
-          - mathcomp/mathcomp:2.0.0-coq-8.17
           - mathcomp/mathcomp:2.0.0-coq-8.18
-          - mathcomp/mathcomp:2.1.0-coq-8.16
-          - mathcomp/mathcomp:2.1.0-coq-8.17
           - mathcomp/mathcomp:2.1.0-coq-8.18
-          - mathcomp/mathcomp:2.2.0-coq-8.16
-          - mathcomp/mathcomp:2.2.0-coq-8.17
           - mathcomp/mathcomp:2.2.0-coq-8.18
           - mathcomp/mathcomp:2.2.0-coq-8.19
           - mathcomp/mathcomp:2.2.0-coq-8.20
-          - mathcomp/mathcomp:2.2.0-coq-dev
           - mathcomp/mathcomp:2.3.0-coq-8.18
           - mathcomp/mathcomp:2.3.0-coq-8.19
           - mathcomp/mathcomp:2.3.0-coq-8.20
-          - mathcomp/mathcomp:2.3.0-coq-dev
-          - mathcomp/mathcomp-dev:coq-8.18
           - mathcomp/mathcomp-dev:coq-8.19
           - mathcomp/mathcomp-dev:coq-8.20
-          - mathcomp/mathcomp-dev:coq-dev
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

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

coq-mathcomp-multinomials.opam

@@ -8,7 +8,7 @@ authors: ["Pierre-Yves Strub"]
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq"                    {(>= "8.16" & < "8.21~") | = "dev"}
+  "coq"                    {(>= "8.18" & < "8.21~") | = "dev"}
   "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.4~") | = "dev"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-bigenough" {(>= "1.0" & < "1.1~") | = "dev"}

src/mpoly.v

@@ -77,7 +77,7 @@
 (* -------------------------------------------------------------------------- *)
 
 (* -------------------------------------------------------------------- *)
-From Coq Require Import Setoid.
+From Corelib Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import choice fintype tuple finfun bigop finset binomial.