diff options
| author | Pierre-Marie Pédrot | 2020-03-06 10:57:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-08 15:31:27 +0100 |
| commit | e0bcbccf437ebee4157fdfdd5cba7b42019ead27 (patch) | |
| tree | be68f0664931c850ac09bb29575210f4c890a9bc /kernel/environ.ml | |
| parent | 4481b95f6f89acd7013b16a345d379dc44d67705 (diff) | |
Ensure that template parameters are shared in the same inductive block.
This could have been at the root of strange behaviours (read unsoundness).
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 |