diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-26 17:22:08 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-26 17:28:47 +0100 |
| commit | 40cc1067dc5353d43ea2f6643cd8ca954e3e8afa (patch) | |
| tree | ddee987212d4cb509ca349718bee617da43104e1 /kernel/indtypes.ml | |
| parent | 5361b02a96704a226b713b6040b67ca01de808fa (diff) | |
Fixing bde12b70 about reporting ill-formed constructor.
For instance, in
Inductive I : nat -> nat -> Prop := C : forall z, let '(x,y) := z in x + y = 0.
the computation of the number of arguments to I was made wrong in bde12b70.
Diffstat (limited to 'kernel/indtypes.ml')
| -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 f9c2a7b0d..49e858315 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -336,7 +336,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor of rel_context * constr list + | LocalNotConstructor of rel_context * int | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -355,11 +355,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 = rel_context_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)))) @@ -548,7 +547,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) |