diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-04 19:15:28 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-04 19:15:28 +0000 |
| commit | 4372b5bc27e7ffcb4bff2cf5c093cdbafeddfe83 (patch) | |
| tree | 0b76ad21b4123268a6338610bad4b2b468c3aac1 /kernel | |
| parent | 6fb58f97c756fcd4841876edc6da4001d23d8bbb (diff) | |
Fixing #2846: Uncaught exception Reduction.NotArity.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16662 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 7 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e0bfb69ae..a69537231 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -45,7 +45,7 @@ type inductive_error = | SameNamesTypes of Id.t | SameNamesConstructors of Id.t | SameNamesOverlap of Id.t list - | NotAnArity of Id.t + | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType @@ -262,7 +262,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 0d3d1bdff..ce789b00e 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -28,7 +28,7 @@ type inductive_error = | SameNamesTypes of Id.t | SameNamesConstructors of Id.t | SameNamesOverlap of Id.t list - | NotAnArity of Id.t + | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType |