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).
---
 pretyping/evarsolve.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/evarsolve.ml')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aafd662f7d..c9ccd668ca 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -78,9 +78,9 @@ let get_polymorphic_positions env sigma f =
   match EConstr.kind sigma f with
   | Ind (ind, u) | Construct ((ind, _), u) ->
     let mib,oib = Inductive.lookup_mind_specif env ind in
-      (match oib.mind_arity with
-      | RegularArity _ -> assert false
-      | TemplateArity templ -> templ.template_param_levels)
+      (match mib.mind_template with
+      | None -> assert false
+      | Some templ -> templ.template_param_levels)
   | _ -> assert false
 
 let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
-- 
cgit v1.2.3