diff --git a/qc/Typeclasses.v b/qc/Typeclasses.v
index f694134..a8c62f5 100644
--- a/qc/Typeclasses.v
+++ b/qc/Typeclasses.v
@@ -890,7 +890,7 @@ Proof. intros. eapply trans3; eassumption. Defined.
 (** The [ssreflect] library defines what it means for a proposition
     [P] to be decidable like this... *)
 
-From mathcomp.ssreflect Require Import ssreflect ssrbool.
+Require Import ssreflect ssrbool.
 
 Print decidable.
 (* ==>