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.
---
 kernel/inferCumulativity.ml | 24 ++++++++----------------
 1 file changed, 8 insertions(+), 16 deletions(-)

(limited to 'kernel/inferCumulativity.ml')

diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 550c81ed82..77abe6b410 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -216,19 +216,11 @@ let infer_inductive env mie =
   let open Entries in
   let params = mie.mind_entry_params in
   let entries = mie.mind_entry_inds in
-  let variances =
-    match mie.mind_entry_variance with
-    | None -> None
-    | Some _ ->
-      let uctx = match mie.mind_entry_universes with
-        | Monomorphic_entry _ -> assert false
-        | Polymorphic_entry (_,uctx) -> uctx
-      in
-      try Some (infer_inductive_core env params entries uctx)
-      with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
-  in
-  { mie with mind_entry_variance = variances }
-
-let dummy_variance = let open Entries in function
-  | Monomorphic_entry _ -> assert false
-  | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant
+  if not mie.mind_entry_cumulative then None
+  else
+    let uctx = match mie.mind_entry_universes with
+      | Monomorphic_entry _ -> assert false
+      | Polymorphic_entry (_,uctx) -> uctx
+    in
+    try Some (infer_inductive_core env params entries uctx)
+    with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
-- 
cgit v1.2.3