From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 kernel/indTyping.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/indTyping.mli')

diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 8841e38636..2598548f3f 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -16,6 +16,7 @@ open Declarations
     Returns:
     - environment with inductives + parameters in rel context
     - abstracted universes
+    - checked variance info
     - parameters
     - for each inductive,
       (arity * constructors) (with params)
@@ -24,7 +25,7 @@ open Declarations
  *)
 val typecheck_inductive : env -> mutual_inductive_entry ->
   env
-  * abstract_inductive_universes
+  * universes * Univ.Variance.t array option
   * Constr.rel_context
   * ((inductive_arity * Constr.types array) *
      (Constr.rel_context * (Constr.rel_context * Constr.types) array) *
-- 
cgit v1.2.3