Merge pull request #119 from proux01/no-stdlib

Remove Stdlib dependency

.github/workflows/docker-action.yml

@@ -17,8 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.0.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.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'

.gitignore

@@ -4,5 +4,7 @@
 *.glob
 *.v.d
 *.aux
-Makefile.*
+.Makefile.coq.d
+Makefile.coq
+Makefile.coq.conf
 *~

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

README.md

@@ -24,7 +24,7 @@ which will be used to subsume notations for finite sets, eventually.
   - Cyril Cohen (initial)
   - Kazuhiko Sakaguchi
 - License: [CeCILL-B](CECILL-B)
-- Compatible Coq versions: Coq 8.16 to 8.20
+- Compatible Coq versions: Coq 8.18 to 8.20
 - Additional dependencies:
   - [MathComp ssreflect 2.0 to 2.3](https://math-comp.github.io)
 - Coq namespace: `mathcomp.finmap`

coq-mathcomp-finmap.opam

@@ -21,7 +21,7 @@ which will be used to subsume notations for finite sets, eventually."""
 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") }
 ]
 

finmap.v

@@ -1,7 +1,7 @@
 (* (c) Copyright 2006-2019 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 
-From Coq Require Import Setoid.
+From Corelib Require Import Setoid.
 From HB Require Import structures.
 Set Warnings "-notation-incompatible-format".
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.

meta.yml

@@ -31,14 +31,10 @@ license:
   file: CECILL-B
 
 supported_coq_versions:
-  text: Coq 8.16 to 8.20
-  opam: '{ (>= "8.16" & < "8.21~") | (= "dev") }'
+  text: Coq 8.18 to 8.20
+  opam: '{ (>= "8.18" & < "8.21~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.0.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'