diff --git a/theories/dfa.v b/theories/dfa.v
index cff26a9..ca0acfb 100644
--- a/theories/dfa.v
+++ b/theories/dfa.v
@@ -1,5 +1,6 @@
 (* Authors: Christian Doczkal and Jan-Oliver Kaiser *)
 (* Distributed under the terms of CeCILL-B. *)
+From Coq Require Import Setoid.
 From mathcomp Require Import all_ssreflect.
 From RegLang Require Import misc languages.
 
diff --git a/theories/setoid_leq.v b/theories/setoid_leq.v
index e146b5b..fba24be 100644
--- a/theories/setoid_leq.v
+++ b/theories/setoid_leq.v
@@ -1,7 +1,7 @@
 (* Author: Christian Doczkal  *)
 (* Distributed under the terms of CeCILL-B. *)
 
-From Coq Require Import Basics Setoid Morphisms.
+From Coq Require Import Basics Setoid Morphisms BinPos.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 
 Set Implicit Arguments.