diff --git a/bigenough.v b/bigenough.v index c164bda..49995d3 100644 --- a/bigenough.v +++ b/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. *) diff --git a/coq-mathcomp-bigenough.opam b/coq-mathcomp-bigenough.opam index c26c70d..69aac11 100644 --- a/coq-mathcomp-bigenough.opam +++ b/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"} ]