diff options
| author | Gaëtan Gilbert | 2020-02-07 13:25:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 13:25:59 +0100 |
| commit | 633d9829d4e3678583c9e1ad161253fb53be1290 (patch) | |
| tree | 4c7edf5c090b369574b68d587787bac4b74d89ba /kernel | |
| parent | adf04f62d3ff5b0651cec2e8596ce3900d3af1eb (diff) | |
| parent | 22b3b961804bea2c8b56cbab9a0c4902bf45c56c (diff) | |
Merge PR #11528: Checker does not rely on Monomorphic fields
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 4 | ||||
| -rw-r--r-- | kernel/declarations.ml | 1 | ||||
| -rw-r--r-- | kernel/declareops.ml | 3 | ||||
| -rw-r--r-- | kernel/indTyping.ml | 2 |
4 files changed, 6 insertions, 4 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index cebbfe4986..f1eb000c88 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -312,14 +312,14 @@ let cook_one_ind ~template_check ~ntypes let arity = abstract_as_type (expmod arity) hyps in let sort = destSort (expmod (mkSort sort)) in RegularArity {mind_user_arity=arity; mind_sort=sort} - | TemplateArity {template_param_levels=levels;template_level} -> + | TemplateArity {template_param_levels=levels;template_level;template_context} -> let sec_levels = CList.map_filter (fun d -> if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d) else None) section_decls in let levels = List.rev_append sec_levels levels in - TemplateArity {template_param_levels=levels;template_level} + TemplateArity {template_param_levels=levels;template_level;template_context} in let mind_arity_ctxt = let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 0b6e59bd5e..c550b0d432 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -32,6 +32,7 @@ type engagement = set_predicativity type template_arity = { template_param_levels : Univ.Level.t option list; template_level : Univ.Universe.t; + template_context : Univ.ContextSet.t; } type ('a, 'b) declaration_arity = diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 27e3f84464..047027984d 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -49,7 +49,8 @@ let map_decl_arity f g = function let hcons_template_arity ar = { template_param_levels = ar.template_param_levels; (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) - template_level = Univ.hcons_univ ar.template_level } + template_level = Univ.hcons_univ ar.template_level; + template_context = Univ.hcons_universe_context_set ar.template_context } let universes_context = function | Monomorphic _ -> Univ.AUContext.empty diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 719eb276df..113ee787f2 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -274,7 +274,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp CErrors.user_err Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") else - TemplateArity {template_param_levels = param_levels; template_level = min_univ} + TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx } in let kelim = allowed_sorts univ_info in |