diff options
| author | Gaëtan Gilbert | 2020-03-10 14:19:30 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-10 14:19:30 +0100 |
| commit | cffb0ed6f58188b8ea01d54a5349d28313b86dc1 (patch) | |
| tree | 21c770ded4937e00419947f4ae31840217ce4978 /kernel/environ.ml | |
| parent | f1188b9a3f32eef7657bb46026447718f6fb6055 (diff) | |
| parent | 74df1a17d7d58d4fa99de58899e08de5bbe97810 (diff) | |
Merge PR #11764: Simplify mutual template polymorphism
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 501ac99ff3..1b5a77cc96 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -590,11 +590,11 @@ let template_polymorphic_ind (mind,i) env = | TemplateArity _ -> true | RegularArity _ -> false -let template_polymorphic_variables (mind,i) env = - match (lookup_mind mind env).mind_packets.(i).mind_arity with - | TemplateArity { Declarations.template_param_levels = l; _ } -> +let template_polymorphic_variables (mind, _) env = + match (lookup_mind mind env).mind_template with + | Some { Declarations.template_param_levels = l; _ } -> List.map_filter (fun level -> level) l - | RegularArity _ -> [] + | None -> [] let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false |