diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-29 17:27:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-29 18:03:50 +0100 |
| commit | 0b644da20c714b01565f88dffcfd51ea8f08314a (patch) | |
| tree | 5a63fe126f7ae1f5d0e9460234291dd3dd55a78b /kernel | |
| parent | 4953a129858a231e64dec636a3bc15a54a0e771c (diff) | |
| parent | 22a2cc1897f0d9f568ebfb807673e84f6ada491a (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index ac665bc25..a8625009c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -340,7 +340,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor of Context.Rel.t * constr list + | LocalNotConstructor of Context.Rel.t * int | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -359,11 +359,10 @@ let explain_ind_err id ntyp env nbpar c err = | LocalNotEnoughArgs kt -> raise (InductiveError (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) - | LocalNotConstructor (paramsctxt,args)-> + | LocalNotConstructor (paramsctxt,nargs)-> let nparams = Context.Rel.nhyps paramsctxt in raise (InductiveError - (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams, - List.length args - nparams))) + (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams,nargs))) | LocalNonPar (n,i,l) -> raise (InductiveError (NonPar (env,c',n,mkRel i, mkRel (l+nbpar)))) @@ -587,7 +586,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname begin match hd with | Rel j when Int.equal j (n + ntypes - i - 1) -> check_correct_par ienv hyps (ntypes - i) largs - | _ -> raise (IllFormedInd (LocalNotConstructor(hyps,largs))) + | _ -> raise (IllFormedInd (LocalNotConstructor(hyps,nargs))) end else if not (List.for_all (noccur_between n ntypes) largs) |