From 8291c83620312550d1ccbe9a304fd43f35724b12 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 22 Mar 2006 09:41:17 +0000 Subject: - Correction bug calcul mind_consnrealargs, introduit à la révision 7833, et que la révision 8644 n'avait pas corrigé dans le bon sens; renommage en mind_consnrealdecls pour éviter la confusion de sens avec mind_nrealargs - Correction de la description du type one_inductive_body - Ajout test avec let-in dans params et dans type constructeur (fichier Case12.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/declarations.ml | 8 ++++---- kernel/declarations.mli | 6 +++--- kernel/indtypes.ml | 5 +++-- kernel/inductive.ml | 2 +- 4 files changed, 11 insertions(+), 10 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 15c234b334..fbd31f24fc 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -118,8 +118,8 @@ type one_inductive_body = { (* Head normalized constructor types so that their conclusion is atomic *) mind_nf_lc : types array; - (* Number of expected (real) arg of the constructors (no let, no params) *) - mind_consnrealargs : int array; + (* Length of the signature of the constructors (with let, w/o params) *) + mind_consnrealdecls : int array; (* Signature of recursive arguments in the constructors *) mind_recargs : wf_paths; @@ -155,7 +155,7 @@ type mutual_inductive_body = { (* Number of expected parameters *) mind_nparams : int; - (* Number of non recursively uniform parameters *) + (* Number of recursively uniform (i.e. ordinary) parameters *) mind_nparams_rec : int; (* The context of parameters (includes let-in declaration) *) @@ -180,7 +180,7 @@ let subst_const_body sub cb = { let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; - mind_consnrealargs = mbp.mind_consnrealargs; + mind_consnrealdecls = mbp.mind_consnrealdecls; mind_typename = mbp.mind_typename; mind_nf_lc = array_smartmap (type_app (subst_mps sub)) mbp.mind_nf_lc; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 10559ffe15..bd689ced37 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -105,8 +105,8 @@ type one_inductive_body = { (* Head normalized constructor types so that their conclusion is atomic *) mind_nf_lc : types array; - (* Number of expected (real) arg of the constructors (no let, no params) *) - mind_consnrealargs : int array; + (* Length of the signature of the constructors (with let, w/o params) *) + mind_consnrealdecls : int array; (* Signature of recursive arguments in the constructors *) mind_recargs : wf_paths; @@ -142,7 +142,7 @@ type mutual_inductive_body = { (* Number of expected parameters *) mind_nparams : int; - (* Number of non recursively uniform parameters *) + (* Number of recursively uniform (i.e. ordinary) parameters *) mind_nparams_rec : int; (* The context of parameters (includes let-in declaration) *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 2398375699..103a5982ef 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -543,7 +543,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in let nf_lc = if nf_lc = lc then lc else nf_lc in let consnrealargs = - Array.map (fun (d,b) -> rel_context_nhyps d - nparamargs) splayed_lc in + Array.map (fun (d,_) -> rel_context_length d - rel_context_length params) + splayed_lc in (* Elimination sorts *) let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in let kelim = allowed_sorts env issmall isunit ar_sort in @@ -568,7 +569,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = mind_sort = ar_sort; mind_kelim = kelim; mind_consnames = Array.of_list cnames; - mind_consnrealargs = consnrealargs; + mind_consnrealdecls = consnrealargs; mind_user_lc = lc; mind_nf_lc = nf_lc; mind_recargs = recarg; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 92b919c7eb..3adbd6e36a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -278,7 +278,7 @@ let check_case_info env indsp ci = if (indsp <> ci.ci_ind) or (mib.mind_nparams <> ci.ci_npar) or - (mip.mind_consnrealargs <> ci.ci_cstr_nargs) + (mip.mind_consnrealdecls <> ci.ci_cstr_nargs) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) (************************************************************************) -- cgit v1.2.3