From 40cc1067dc5353d43ea2f6643cd8ca954e3e8afa Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 26 Jan 2016 17:22:08 +0100 Subject: 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. --- kernel/indtypes.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'kernel/indtypes.ml') 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) -- cgit v1.2.3