From e0bcbccf437ebee4157fdfdd5cba7b42019ead27 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Mar 2020 10:57:19 +0100
Subject: Ensure that template parameters are shared in the same inductive
 block.

This could have been at the root of strange behaviours (read unsoundness).
---
 kernel/environ.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/environ.ml')

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
-- 
cgit v1.2.3