Ensure that template parameters are shared in the same inductive block.

This could have been at the root of strange behaviours (read unsoundness).

2 files changed, 8 insertions, 4 deletions

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)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a4406aeba1..01994a35c7 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -681,13 +681,17 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
   match mip.mind_arity with
   | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity)
   | TemplateArity ar ->
+    let templ = match mib.mind_template with
+    | None -> assert false
+    | Some t -> t
+    in
     let _,scl = splay_arity env sigma conclty in
     let scl = EConstr.ESorts.kind sigma scl in
     let ctx = List.rev mip.mind_arity_ctxt in
     let evdref = ref sigma in
     let ctx =
       instantiate_universes
-        env evdref scl ar.template_level (ctx,ar.template_param_levels) in
+        env evdref scl ar.template_level (ctx,templ.template_param_levels) in
       !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl))
 
 let type_of_projection_constant env (p,u) =