From fb1eb17d40febf3f4927568921b64b7a8c7ca028 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 26 Sep 2012 20:31:35 +0000
Subject: Incorrect comment

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15835 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

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 =
-- 
cgit v1.2.3