transcript: improved debuugging facilities

[helm.git] / helm / software / matita / contribs / procedural / Coq / Logic / ClassicalDescription.mma

diff --git a/helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma b/helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma
index 7ab50d0141c6eea18a84f33f92d9f1ea9f8f3999..82db6eb1f8a962abdbb51a479922297412eabb74 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma
@@ -39,7 +39,7 @@ include "Coq.ma".
     implies a strongly classical world. Especially it conflicts with
     impredicativity of Set, knowing that true<>false in Set.
 
-    [1] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical
+    [1] Laurent Chicli, Lo\239\c Pottier, Carlos Simpson, Mathematical
     Quotients and Quotient Types in Coq, Proceedings of TYPES 2002,
     Lecture Notes in Computer Science 2646, Springer Verlag.
 *)