From 441bea723c511ed9e18ef005678bd01242b45c49 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Dec 2017 13:57:10 +0100 Subject: Returning instance instead of substitution in universe context abstraction. This datatype enforces stronger invariants, e.g. that we only have in the substitution codomain a connex interval of variables from 0 to n - 1. --- kernel/univ.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/univ.mli') diff --git a/kernel/univ.mli b/kernel/univ.mli index 459394439..324167890 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -470,9 +470,9 @@ val subst_instance_universe : Instance.t -> Universe.t -> Universe.t val make_instance_subst : Instance.t -> universe_level_subst val make_inverse_instance_subst : Instance.t -> universe_level_subst -val abstract_universes : UContext.t -> universe_level_subst * AUContext.t +val abstract_universes : UContext.t -> Instance.t * AUContext.t -val abstract_cumulativity_info : CumulativityInfo.t -> universe_level_subst * ACumulativityInfo.t +val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t val make_abstract_instance : AUContext.t -> Instance.t -- cgit v1.2.3