fix path to boolp in contra.v

math-comp · Dec 23, 2023 · 1035292 · 1035292
1 parent 9561644
commit 1035292
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.