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.mli | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel/inferCumulativity.mli')

diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index a234e334d1..2bddfe21e2 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -9,6 +9,4 @@
 (************************************************************************)
 
 val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
-  Entries.mutual_inductive_entry
-
-val dummy_variance : Entries.universes_entry -> Univ.Variance.t array
+  Univ.Variance.t array option
-- 
cgit v1.2.3