Merge pull request #14 from proux01/mc1415

Adapt to math-comp/math-comp#1415

Author: CohenCyril

bigenough.v

@@ -1,8 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
+From mathcomp Require Import ssreflect ssrfun ssrbool.
+From mathcomp Require Import eqtype ssrnat seq choice fintype.
 
 (****************************************************************************)
 (* This is a small library to do epsilon - N reasoning.                     *)

coq-mathcomp-bigenough.opam

@@ -21,7 +21,7 @@ library."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.10" & < "8.15~") | (= "dev")}
+  "coq" {(>= "8.10" & < "9.1~") | (= "dev")}
   "coq-mathcomp-ssreflect" {>= "1.6"}
 ]