From d81375002501cdc6e677244557a87b2f1a445e5b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 17 Jan 2020 14:32:28 +0100
Subject: Check instance length in type_of_{inductive,constructor}

---
 vernac/assumptions.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'vernac')

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