diff --git a/classical/contra.v b/classical/contra.v
index a2691ee7ab..f11935631a 100644
--- a/classical/contra.v
+++ b/classical/contra.v
@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-Require Import boolp.
+From mathcomp Require Import boolp.
 
 Set Implicit Arguments.
 Unset Strict Implicit.