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.