From 1035292dca39a52af8a04a3e20e16a00974dd9d9 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Sat, 23 Dec 2023 14:48:38 +0100 Subject: [PATCH] fix path to boolp in contra.v --- classical/contra.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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.