diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-12-12 16:37:03 -0500 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-12-19 08:51:35 +0100 |
| commit | a56e966162aee59b6044c1fd1d9d4e43c33eba35 (patch) | |
| tree | eccf53c5437280c2b8b96f9b2a53dd5e52c572ec /theories/Logic | |
| parent | fe4a29ef11c2db8ffb26ef0ba0775fc939471ac9 (diff) | |
Fix a typo in Hurkens.v comment
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/Hurkens.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. *) |