diff options
| author | msozeau | 2012-09-26 20:31:35 +0000 |
|---|---|---|
| committer | msozeau | 2012-09-26 20:31:35 +0000 |
| commit | fb1eb17d40febf3f4927568921b64b7a8c7ca028 (patch) | |
| tree | bbbc6869530d3205900ae9581aef112915b6f790 /kernel | |
| parent | 33509e348a6c9f505a6ebf714d8b142fc9df62a0 (diff) | |
Incorrect comment
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15835 85f007b7-540e-0410-9357-904b9bb8a0f7
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 = |