diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 6 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 6 | ||||
| -rw-r--r-- | kernel/univ.ml | 7 | ||||
| -rw-r--r-- | kernel/univ.mli | 4 |
4 files changed, 10 insertions, 13 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 2d74f99c15..20c90bc05a 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -852,13 +852,11 @@ let abstract_inductive_universes iu = match iu with | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) | Polymorphic_ind_entry (nas, ctx) -> - let () = assert (Int.equal (List.length nas) (UContext.size ctx)) in - let (inst, auctx) = Univ.abstract_universes ctx in + let (inst, auctx) = Univ.abstract_universes nas ctx in let inst = Univ.make_instance_subst inst in (inst, Polymorphic_ind auctx) | Cumulative_ind_entry (nas, cumi) -> - let (inst, acumi) = Univ.abstract_cumulativity_info cumi in - let () = assert (Int.equal (List.length nas) (Instance.length inst)) in + let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in let inst = Univ.make_instance_subst inst in (inst, Cumulative_ind acumi) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 4759625e8a..35fa871b4e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -69,8 +69,7 @@ let abstract_constant_universes = function | Monomorphic_const_entry uctx -> Univ.empty_level_subst, Monomorphic_const uctx | Polymorphic_const_entry (nas, uctx) -> - let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in - let sbst, auctx = Univ.abstract_universes uctx in + let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in sbst, Polymorphic_const auctx @@ -160,9 +159,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = unconditionally export side-effects from polymorphic definitions, i.e. [trust] is always [Pure]. *) let () = assert (Univ.ContextSet.is_empty ctx) in - let () = assert (Int.equal (List.length nas) (Univ.UContext.size uctx)) in let env = push_context ~strict:false uctx env in - let sbst, auctx = Univ.abstract_universes uctx in + let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in env, sbst, Polymorphic_const auctx in diff --git a/kernel/univ.ml b/kernel/univ.ml index 35566019a8..a8359bc4a7 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1150,8 +1150,9 @@ let make_inverse_instance_subst i = let make_abstract_instance (ctx, _) = Array.mapi (fun i _l -> Level.var i) ctx -let abstract_universes ctx = +let abstract_universes nas ctx = let instance = UContext.instance ctx in + let () = assert (Int.equal (List.length nas) (Instance.length instance)) in let subst = make_instance_subst instance in let cstrs = subst_univs_level_constraints subst (UContext.constraints ctx) @@ -1159,8 +1160,8 @@ let abstract_universes ctx = let ctx = UContext.make (instance, cstrs) in instance, ctx -let abstract_cumulativity_info (univs, variance) = - let subst, univs = abstract_universes univs in +let abstract_cumulativity_info nas (univs, variance) = + let subst, univs = abstract_universes nas univs in subst, (univs, variance) let rec compact_univ s vars i u = diff --git a/kernel/univ.mli b/kernel/univ.mli index bc902d8f4b..e665ed94e7 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -469,8 +469,8 @@ val make_instance_subst : Instance.t -> universe_level_subst val make_inverse_instance_subst : Instance.t -> universe_level_subst -val abstract_universes : UContext.t -> Instance.t * AUContext.t -val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t +val abstract_universes : Names.Name.t list -> UContext.t -> Instance.t * AUContext.t +val abstract_cumulativity_info : Names.Name.t list -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t (** TODO: move universe abstraction out of the kernel *) val make_abstract_instance : AUContext.t -> Instance.t |