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)

---
 checker/checkInductive.ml | 3 ++-
 checker/checker.ml        | 4 +++-
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'checker')

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 7bb714aa17..7513564cf0 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -69,6 +69,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
   in
   let mind_entry_template = Array.exists check_template mb.mind_packets in
   let () = if mind_entry_template then assert (Array.for_all check_template mb.mind_packets) in
+  let mind_entry_variance = Option.map (Array.map (fun v -> Some v)) mb.mind_variance in
   {
     mind_entry_record;
     mind_entry_finite = mb.mind_finite;
@@ -76,7 +77,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     mind_entry_inds;
     mind_entry_universes;
     mind_entry_template;
-    mind_entry_cumulative= Option.has_some mb.mind_variance;
+    mind_entry_variance;
     mind_entry_private = mb.mind_private;
   }
 
diff --git a/checker/checker.ml b/checker/checker.ml
index e2c90e2b93..08d92bb7b3 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -298,7 +298,9 @@ let explain_exn = function
       | DisallowedSProp -> str"DisallowedSProp"
       | BadRelevance -> str"BadRelevance"
       | BadInvert -> str"BadInvert"
-      | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
+      | UndeclaredUniverse _ -> str"UndeclaredUniverse"
+      | BadVariance _ -> str "BadVariance"
+      ))
 
   | InductiveError e ->
       hov 0 (str "Error related to inductive types")
-- 
cgit v1.2.3