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

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 1be86f2bf8..6325779675 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -185,8 +185,8 @@ let make_subst =
 
 exception SingletonInductiveBecomesProp of Id.t
 
-let instantiate_universes ctx ar args =
-  let subst = make_subst (ctx,ar.template_param_levels,args) in
+let instantiate_universes ctx (templ, ar) args =
+  let subst = make_subst (ctx,templ.template_param_levels,args) in
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
@@ -215,8 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps =
   match mip.mind_arity with
   | RegularArity a -> subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
+    let templ = match mib.mind_template with
+    | None -> assert false
+    | Some t -> t
+    in
     let ctx = List.rev mip.mind_arity_ctxt in
-    let ctx,s = instantiate_universes ctx ar paramtyps in
+    let ctx,s = instantiate_universes ctx (templ, ar) paramtyps in
       (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
          the situation where a non-Prop singleton inductive becomes Prop
          when applied to Prop params *)
-- 
cgit v1.2.3