diff options
| author | Gaëtan Gilbert | 2020-01-17 14:32:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-12 13:13:24 +0100 |
| commit | d81375002501cdc6e677244557a87b2f1a445e5b (patch) | |
| tree | 45e3f1f5a93e9676952637eec853a510f25f2919 /kernel/inductive.ml | |
| parent | 6c1de3455d5cd79958a8e26ac728f7d5d1b8d025 (diff) | |
Check instance length in type_of_{inductive,constructor}
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ca4fea45c5..5d8e1f0fdb 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -198,7 +198,14 @@ let relevance_of_inductive env ind = let _, mip = lookup_mind_specif env ind in mip.mind_relevance -let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps = +let check_instance mib u = + if not (match mib.mind_universes with + | Monomorphic _ -> Instance.is_empty u + | Polymorphic uctx -> Instance.length u = AUContext.size uctx) + then CErrors.anomaly Pp.(str "bad instance length on mutind.") + +let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = + check_instance mib u; match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> @@ -244,6 +251,7 @@ let max_inductive_sort = (* Type of a constructor *) let type_of_constructor (cstr, u) (mib,mip) = + check_instance mib u; let ind = inductive_of_constructor cstr in let specif = mip.mind_user_lc in let i = index_of_constructor cstr in |