diff options
Diffstat (limited to 'checker/indtypes.ml')
| -rw-r--r-- | checker/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 49d78a7a6..c8373737c 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -211,7 +211,7 @@ let allowed_sorts issmall isunit s = (* Unitary/empty Prop: elimination to all sorts are realizable *) (* unless the type is large. If it is large, forbids large elimination *) - (* which otherwise allows to simulate the inconsistent system Type:Type *) + (* which otherwise allows simulating the inconsistent system Type:Type *) | InProp when isunit -> if issmall then all_sorts else small_sorts (* Other propositions: elimination only to Prop *) |