diff options
| author | Hugo Herbelin | 2015-10-22 22:25:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-22 22:37:44 +0200 |
| commit | 273005ac85e9ae0c23328e243edeadfc8dcaf8bb (patch) | |
| tree | 4084d81a08d34d541122fb3fc91574bce1003ba5 | |
| parent | 95b04506542064fbda7a61c4b6ce276a668d25bd (diff) | |
Fixing a bug in reporting ill-formed inductive.
Was introduced in b06d3badb (15 Jul 2015).
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/Inductive.out | 3 | ||||
| -rw-r--r-- | test-suite/output/Inductive.v | 3 |
3 files changed, 7 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5d7a0bbf00..8b03df64c6 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' diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out new file mode 100644 index 0000000000..e912003f03 --- /dev/null +++ b/test-suite/output/Inductive.out @@ -0,0 +1,3 @@ +The command has indeed failed with message: +Last occurrence of "list'" must have "A" as 1st argument in + "A -> list' A -> list' (A * A)%type". diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v new file mode 100644 index 0000000000..8db8956e32 --- /dev/null +++ b/test-suite/output/Inductive.v @@ -0,0 +1,3 @@ +Fail Inductive list' (A:Set) : Set := +| nil' : list' A +| cons' : A -> list' A -> list' (A*A). |