From f3a6d9dce4d1c291dbaa03bd0e4ed5f33646bff0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 30 Dec 2019 12:15:21 +0100
Subject: generate variance data for section universes (not yet used)

preparation for direct discharge
---
 kernel/indTyping.mli | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'kernel/indTyping.mli')

diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 5c04e860a2..8dea8f046d 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -17,6 +17,7 @@ open Declarations
     - environment with inductives + parameters in rel context
     - abstracted universes
     - checked variance info
+      (variance for section universes is at the beginning of the array)
     - record entry (checked to be OK)
     - parameters
     - for each inductive,
@@ -24,9 +25,11 @@ open Declarations
       * (indices * splayed constructor types) (both without params)
       * top allowed elimination
  *)
-val typecheck_inductive : env -> mutual_inductive_entry ->
-  env
-  * universes * Univ.Variance.t array option
+val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
+  -> mutual_inductive_entry
+  -> env
+  * universes
+  * Univ.Variance.t array option
   * Names.Id.t array option option
   * Constr.rel_context
   * ((inductive_arity * Constr.types array) *
-- 
cgit v1.2.3