From db0918bfa5089f9ab44374504cbd0ddc758ea1e5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 20 Feb 2018 00:27:40 +0100
Subject: Cumulativity: improve treatment of irrelevant universes.

In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
---
 kernel/reduction.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel/reduction.mli')

diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index ad52c93f62..14e4270b7c 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -41,7 +41,8 @@ type 'a universe_compare =
   { (* Might raise NotConvertible *)
     compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a }
+    compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
+      Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
 
 type 'a universe_state = 'a * 'a universe_compare
 
@@ -49,7 +50,7 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 
 type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 
-val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t ->
+val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array ->
   Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
 
 val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
-- 
cgit v1.2.3