diff options
| author | Pierre-Marie Pédrot | 2020-02-13 10:44:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-13 10:44:55 +0100 |
| commit | 9510d6f42aadc6435e2e444dcab9a9d3cffddc36 (patch) | |
| tree | 7bc82c0f9462bd802e526fb231ea1e7485890d4e /kernel | |
| parent | 36a93a58446d487a136d999649d66ca7d4b09f70 (diff) | |
| parent | d81375002501cdc6e677244557a87b2f1a445e5b (diff) | |
Merge PR #11424: Check instance length in type_of_{inductive,constructor}
Reviewed-by: ppedrot
Diffstat (limited to 'kernel')
| -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 |