diff options
| -rw-r--r-- | kernel/declarations.ml | 2 | ||||
| -rw-r--r-- | kernel/declarations.mli | 1 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 3 | ||||
| -rw-r--r-- | kernel/inductive.ml | 3 | ||||
| -rw-r--r-- | kernel/term.ml | 1 | ||||
| -rw-r--r-- | kernel/term.mli | 1 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 1 |
7 files changed, 11 insertions, 1 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 82864bbe4..9d2548b17 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -89,6 +89,7 @@ type one_inductive_body = { mind_sort : sorts; mind_kelim : sorts_family list; mind_consnames : identifier array; + mind_consnrealargs : int array; mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *) mind_user_lc : types array; mind_recargs : wf_paths; @@ -122,6 +123,7 @@ let subst_const_body sub cb = { let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; + mind_consnrealargs = mbp.mind_consnrealargs; 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 cdb394380..d4f840b14 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -76,6 +76,7 @@ type one_inductive_body = { mind_sort : sorts; mind_kelim : sorts_family list; mind_consnames : identifier array; + mind_consnrealargs : int array; (* length of constructs, let-in included *) mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *) mind_user_lc : types array; mind_recargs : wf_paths; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5237b93db..83928b6cc 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -534,6 +534,8 @@ let build_inductive env env_ar params record finite inds nmr recargs cst = let nf_lc = array_map2 (fun (d,b) c -> it_mkProd_or_LetIn b d) splayed_lc lc in let nf_lc = if nf_lc = lc then lc else nf_lc in + let consnrealargs = + Array.map (fun (d,b) -> List.length d - nparamargs) 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 @@ -558,6 +560,7 @@ let build_inductive env env_ar params record finite inds nmr recargs cst = mind_sort = ar_sort; mind_kelim = kelim; mind_consnames = Array.of_list cnames; + mind_consnrealargs = consnrealargs; mind_user_lc = lc; mind_nf_lc = nf_lc; mind_recargs = recarg; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index af237d1d1..06a3d5ecf 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -278,7 +278,8 @@ let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if (indsp <> ci.ci_ind) or - (mib.mind_nparams <> ci.ci_npar) + (mib.mind_nparams <> ci.ci_npar) or + (mip.mind_consnrealargs <> ci.ci_cstr_nargs) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) (************************************************************************) diff --git a/kernel/term.ml b/kernel/term.ml index f2fe38479..f83e69fcf 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -33,6 +33,7 @@ type case_printing = type case_info = { ci_ind : inductive; ci_npar : int; + ci_cstr_nargs : int array; (* number of real args of each constructor *) ci_pp_info : case_printing (* not interpreted by the kernel *) } diff --git a/kernel/term.mli b/kernel/term.mli index 70388808a..c0c57959f 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -50,6 +50,7 @@ type case_printing = type case_info = { ci_ind : inductive; ci_npar : int; + ci_cstr_nargs : int array; (* number of real args of each constructor *) ci_pp_info : case_printing (* not interpreted by the kernel *) } diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 813a6a269..f8f0e45bc 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -116,6 +116,7 @@ let make_case_info env ind style pats_source = source = pats_source } in { ci_ind = ind; ci_npar = mib.mind_nparams; + ci_cstr_nargs = mip.mind_consnrealargs; ci_pp_info = print_info } let make_default_case_info env style ind = |