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.

1 files changed, 1 insertions, 1 deletions

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;
   }