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/univ.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/univ.mli') diff --git a/kernel/univ.mli b/kernel/univ.mli index ce617932c..629d83fb8 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -312,6 +312,9 @@ type universe_instance = Instance.t val enforce_eq_instances : Instance.t constraint_function +val enforce_eq_variance_instances : Variance.t array -> Instance.t constraint_function +val enforce_leq_variance_instances : Variance.t array -> Instance.t constraint_function + type 'a puniverses = 'a * Instance.t val out_punivs : 'a puniverses -> 'a val in_punivs : 'a -> 'a puniverses -- cgit v1.2.3