diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-22 22:25:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-22 22:37:44 +0200 |
| commit | 273005ac85e9ae0c23328e243edeadfc8dcaf8bb (patch) | |
| tree | 4084d81a08d34d541122fb3fc91574bce1003ba5 /kernel/indtypes.ml | |
| parent | 95b04506542064fbda7a61c4b6ce276a668d25bd (diff) | |
Fixing a bug in reporting ill-formed inductive.
Was introduced in b06d3badb (15 Jul 2015).
Diffstat (limited to 'kernel/indtypes.ml')
| -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 5d7a0bbf0..8b03df64c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -390,7 +390,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | _::hyps -> match kind_of_term (whd_betadeltaiota env lpar.(k)) with | Rel w when Int.equal w index -> check (k-1) (index+1) hyps - | _ -> raise (IllFormedInd (LocalNonPar (k+1, index, l))) + | _ -> raise (IllFormedInd (LocalNonPar (k+1, index-n+nhyps+1, l))) in check (nparams-1) (n-nhyps) hyps; if not (Array.for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' |