Merge PR #11424: Check instance length in type_of_{inductive,constructor}

Reviewed-by: ppedrot

1 files changed, 9 insertions, 1 deletions

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 9f92eba729..fb61a1089f 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -240,8 +240,16 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
      (* Build the context of all arities *)
      let arities_ctx =
        let global_env = Global.env () in
+       let instance =
+         let open Univ in
+         Instance.of_array
+           (Array.init
+              (AUContext.size
+                 (Declareops.inductive_polymorphic_context mib))
+              Level.var)
+       in
        Array.fold_left (fun accu oib ->
-          let pspecif = Univ.in_punivs (mib, oib) in
+          let pspecif = ((mib, oib), instance) in
           let ind_type = Inductive.type_of_inductive global_env pspecif in
           let indr = oib.mind_relevance in
           let ind_name = Name oib.mind_typename in