diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/context.ml | 8 | ||||
| -rw-r--r-- | kernel/context.mli | 2 | ||||
| -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 |
6 files changed, 10 insertions, 10 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 7e394da2ed..500ed20343 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -196,12 +196,10 @@ struct (** Return a new rel-context enriched by with a given inner-most declaration. *) let add d ctx = d :: ctx - (** Return the number of {e local declarations} in a given context. *) + (** Return the number of {e local declarations} in a given rel-context. *) let length = List.length - (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] - with n = |Δ| and with the local definitions of [Γ] skipped in - [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) + (** Return the number of {e local assumptions} in a given rel-context. *) let nhyps ctx = let open Declaration in let rec nhyps acc = function @@ -413,7 +411,7 @@ struct (** empty named-context *) let empty = [] - (** empty named-context *) + (** Return a new named-context enriched by with a given inner-most declaration. *) let add d ctx = d :: ctx (** Return the number of {e local declarations} in a given named-context. *) diff --git a/kernel/context.mli b/kernel/context.mli index 8f233613da..04aa039a01 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -129,7 +129,7 @@ sig (** Return a new rel-context enriched by with a given inner-most declaration. *) val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt - (** Return the number of {e local declarations} in a given context. *) + (** Return the number of {e local declarations} in a given rel-context. *) val length : ('c, 't) pt -> int (** Check whether given two rel-contexts are equal. *) 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 |