From 65c8d91cd4c11b8de44f0b23cd44a3303cd54d4e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 27 Oct 2014 07:21:09 +0100
Subject: Fix some typos in comments.

---
 theories/Logic/Hurkens.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 34dc954ec6..6896b2d577 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -116,7 +116,7 @@ Section Paradox.
 (** ** Axiomatisation of impredicative universes in a Martin-Löf style *)
 
 (** System U- has two impredicative universes. In the proof of the
-    paradox they are slightly asymetric (in particular the reduction
+    paradox they are slightly asymmetric (in particular the reduction
     rules of the small universe are not needed).  Therefore, the
     axioms are duplicated allowing for a weaker requirement than the
     actual system U-. *)
-- 
cgit v1.2.3