From c5c25ce2bb07547af1b93ce02a74078441ac8fc7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 18 May 2026 10:59:50 +0900 Subject: [PATCH] fix #1965 Co-authored-by: @fblanqui --- classical/boolp.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/classical/boolp.v b/classical/boolp.v index b55980e8d7..290b102779 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -13,7 +13,7 @@ From mathcomp Require internal_Eqdep_dec. (* # Classical Logic *) (* *) (* This file provides the axioms of classical logic and tools to perform *) -(* classical reasoning in the Mathematical Compnent framework. The three *) +(* classical reasoning in the Mathematical Component framework. The three *) (* axioms are taken from the standard library of Coq, more details can be *) (* found in Section 5 of *) (* - R. Affeldt, C. Cohen, D. Rouhling. Formalization Techniques for *)