diff options
Diffstat (limited to 'vernac/assumptions.ml')
| -rw-r--r-- | vernac/assumptions.ml | 10 |
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 |