Merge PR #12653: Syntax for specifying cumulative inductives

Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: ppedrot

1 files changed, 8 insertions, 3 deletions

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index b2520b780f..33ee8c325a 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -369,15 +369,20 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
         data, Some None
   in
 
-  let variance = if not mie.mind_entry_cumulative then None
-    else match mie.mind_entry_universes with
+  let variance = match mie.mind_entry_variance with
+    | None -> None
+    | Some variances ->
+      match mie.mind_entry_universes with
       | Monomorphic_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
+        let univs = Array.map2 (fun a b -> a,b) univs variances in
         let univs = match sec_univs with
           | None -> univs
-          | Some sec_univs -> Array.append sec_univs univs
+          | Some sec_univs ->
+            let sec_univs = Array.map (fun u -> u, None) sec_univs in
+            Array.append sec_univs univs
         in
         let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in
         Some variances