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/indtypes.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1f2ae0b6c..b117f8714 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -879,9 +879,13 @@ let abstract_inductive_universes iu = match iu with | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) | Polymorphic_ind_entry ctx -> - let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx) + let (inst, auctx) = Univ.abstract_universes ctx in + let inst = Univ.make_instance_subst inst in + (inst, Polymorphic_ind auctx) | Cumulative_ind_entry cumi -> - let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi) + let (inst, acumi) = Univ.abstract_cumulativity_info cumi in + let inst = Univ.make_instance_subst inst in + (inst, Cumulative_ind acumi) let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in -- cgit v1.2.3