From a56e966162aee59b6044c1fd1d9d4e43c33eba35 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 12 Dec 2016 16:37:03 -0500 Subject: Fix a typo in Hurkens.v comment --- theories/Logic/Hurkens.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Logic') diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 841f843c0..56e03e965 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -562,7 +562,7 @@ End Paradox. End NoRetractFromSmallPropositionToProp. -(** * Large universes are no retracts of [Prop]. *) +(** * Large universes are not retracts of [Prop]. *) (** The existence in the Calculus of Constructions with universes of a retract from some [Type] universe into [Prop] is inconsistent. *) -- cgit v1.2.3