From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 kernel/indtypes.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/indtypes.mli')

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 0477df82..90ae70c3 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: indtypes.mli 10425 2008-01-05 17:04:16Z herbelin $ i*)
+(*i $Id: indtypes.mli 11784 2009-01-14 11:36:32Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -33,6 +33,7 @@ type inductive_error =
   | SameNamesOverlap of identifier list
   | NotAnArity of identifier
   | BadEntry
+  | LargeNonPropInductiveNotInType
 
 exception InductiveError of inductive_error
 
-- 
cgit v1.2.3