From ccb78dc6c0fbf8f883ea73e1f358aa45f8e5b259 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 13 Feb 2025 14:58:55 +0100 Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1343 --- theories/PFsection1.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/PFsection1.v b/theories/PFsection1.v index 51cdeb4..414a05b 100644 --- a/theories/PFsection1.v +++ b/theories/PFsection1.v @@ -1,5 +1,6 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) +From Coq Require Import RelationClasses. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. From mathcomp Require Import div choice fintype tuple finfun bigop prime finset. From mathcomp Require Import order.