From 9990bea3e163850c0ac4dca982c73d2b2bc19a38 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 7 Jul 2020 14:25:20 +0200
Subject: Infrastructure for cumulative inductive syntax (no grammar extension
 yet)

---
 kernel/indTyping.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'kernel/indTyping.ml')

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