diff options
Diffstat (limited to 'kernel/indTyping.ml')
| -rw-r--r-- | kernel/indTyping.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 3f2f9f4fc0..591cd050a5 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -276,7 +276,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp let kelim = allowed_sorts univ_info in (arity,lc), (indices,splayed_lc), kelim -let typecheck_inductive env (mie:mutual_inductive_entry) = +let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let () = match mie.mind_entry_inds with | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.") | _ -> () @@ -341,7 +341,12 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.") | Polymorphic_entry (_,uctx) -> let univs = Instance.to_array @@ UContext.instance uctx in - Some (InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds) + let univs = match sec_univs with + | None -> univs + | Some sec_univs -> Array.append sec_univs univs + in + let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in + Some variances in (* Abstract universes *) |