From 4f1d657f42957d0c2d115424564eedf599584cbc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 29 Oct 2019 13:50:47 +0100
Subject: Remove variance info from inductive entries, infer in indtyping

It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
---
 checker/checkInductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index d20eea7874..06ee4fcc7a 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -61,7 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     mind_entry_params = mb.mind_params_ctxt;
     mind_entry_inds;
     mind_entry_universes;
-    mind_entry_variance = mb.mind_variance;
+    mind_entry_cumulative= Option.has_some mb.mind_variance;
     mind_entry_private = mb.mind_private;
   }
 
-- 
cgit v1.2.3