diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-13 13:57:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-30 19:19:03 +0100 |
| commit | 441bea723c511ed9e18ef005678bd01242b45c49 (patch) | |
| tree | bbe502a899b3b1fa16cb91a7372a2bf2c601ec83 /kernel/indtypes.ml | |
| parent | 6e49d0bee79cd68495955deb115b495fb01f01fd (diff) | |
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.
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 8 |
1 files changed, 6 insertions, 2 deletions
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 |