From 606d7fb7d38d52fbe5b6d19c72c2cc25cb1ce775 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 1 May 2025 16:23:58 +0200 Subject: [PATCH 1/2] Adapt to https://github.com/math-comp/math-comp/pull/1415 --- bigenough.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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. *) From b1c8ebb88660ab81e1d61afd982abffacd52e6d1 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 1 May 2025 17:04:12 +0200 Subject: [PATCH 2/2] Update opam file --- coq-mathcomp-bigenough.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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"} ]