diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 3199d0faa5..1c12c9e244 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -146,7 +146,7 @@ let small_unit constrsinfos = *) let extract_level (_,_,_,lc,lev) = - (* Enforce that the level is not in Prop if more than two constructors *) + (* Enforce that the level is not in Prop if more than one constructor *) if Array.length lc >= 2 then sup type0_univ lev else lev let inductive_levels arities inds = |