diff options
Diffstat (limited to 'theories')
| -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 5f1d5232f..d40882fbf 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -333,7 +333,7 @@ End NoRetractToImpredicativeUniverse. (** * Prop is not a retract *) (** The existence in the pure Calculus of Constructions of a retract - from Prop into a small type of Prop is inconsistent. This is a + from [Prop] into a small type of [Prop] is inconsistent. This is a special case of the previous result. *) Module NoRetractFromSmallPropositionToProp. |