From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 19 Jan 2014 15:09:23 +0100
Subject: Imported Upstream version 8.4pl3dfsg

---
 kernel/cbytecodes.mli | 2 +-
 kernel/csymtable.mli  | 2 +-
 kernel/indtypes.ml    | 7 +++++--
 kernel/indtypes.mli   | 2 +-
 kernel/univ.ml        | 2 +-
 5 files changed, 9 insertions(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index da34d81e..dc2220c1 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cbytecodes.mli 15714 2012-08-08 18:54:37Z herbelin $ *)
+(* $Id$ *)
 
 open Names
 open Term
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 565c31ae..179e4820 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: csymtable.mli 15714 2012-08-08 18:54:37Z herbelin $ *)
+(* $Id$ *)
 
 open Names
 open Term
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0dd2cd69..9ca838fc 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -42,7 +42,7 @@ type inductive_error =
   | SameNamesTypes of identifier
   | SameNamesConstructors of identifier
   | SameNamesOverlap of identifier list
-  | NotAnArity of identifier
+  | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
 
@@ -254,7 +254,10 @@ let typecheck_inductive env mie =
   let ind_min_levels = inductive_levels arities inds in
   let inds, cst =
     array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst ->
-      let sign, s = dest_arity env full_arity in
+      let sign, s =
+        try dest_arity env full_arity
+        with NotArity -> raise (InductiveError (NotAnArity (env, full_arity)))
+      in
       let status,cst = match s with
       | Type u when ar_level <> None (* Explicitly polymorphic *)
             && no_upper_constraints u cst ->
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 4d71a81d..077a2b4f 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -28,7 +28,7 @@ type inductive_error =
   | SameNamesTypes of identifier
   | SameNamesConstructors of identifier
   | SameNamesOverlap of identifier list
-  | NotAnArity of identifier
+  | NotAnArity of env * constr
   | BadEntry
   | LargeNonPropInductiveNotInType
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 028eaeb4..e8c1fed9 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -161,7 +161,7 @@ let type0_univ = Atom UniverseLevel.Set
 
 let is_type0_univ = function
   | Atom UniverseLevel.Set -> true
-  | Max ([UniverseLevel.Set], []) -> warning "Non canonical Set"; true
+  | Max ([UniverseLevel.Set], []) -> msg_warn "Non canonical Set"; true
   | u -> false
 
 let is_univ_variable = function
-- 
cgit v1.2.3