diff options
| -rw-r--r-- | interp/modintern.ml | 2 | ||||
| -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 | ||||
| -rw-r--r-- | library/lib.ml | 22 | ||||
| -rw-r--r-- | vernac/record.ml | 3 |
7 files changed, 32 insertions, 18 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index 93aa271e8b..60056dfd90 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -108,7 +108,7 @@ let transl_with_decl env base kind = function let poly = lookup_polymorphism env base kind fqid in begin match UState.check_univ_decl ~poly ectx udecl with | Entries.Polymorphic_const_entry (nas, ctx) -> - let inst, ctx = Univ.abstract_universes ctx in + let inst, ctx = Univ.abstract_universes nas ctx in let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in let c = EConstr.to_constr sigma c in WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty 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 diff --git a/library/lib.ml b/library/lib.ml index 690a4fd53d..ccf3b4d068 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -479,7 +479,24 @@ let instance_from_variable_context = let named_of_variable_context = List.map fst - + +let name_instance inst = + (** FIXME: this should probably be done at an upper level, by storing the + name information in the section data structure. *) + let map lvl = match Univ.Level.name lvl with + | None -> (* Having Prop/Set/Var as section universes makes no sense *) + assert false + | Some na -> + try + let qid = Nametab.shortest_qualid_of_universe na in + Name (Libnames.qualid_basename qid) + with Not_found -> + (** Best-effort naming from the string representation of the level. + See univNames.ml for a similar hack. *) + Name (Id.of_string_soft (Univ.Level.to_string lvl)) + in + Array.map_to_list map (Univ.Instance.to_array inst) + let add_section_replacement f g poly hyps = match !sectab with | [] -> () @@ -488,7 +505,8 @@ let add_section_replacement f g poly hyps = let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let inst = Univ.UContext.instance ctx in - let subst, ctx = Univ.abstract_universes ctx in + let nas = name_instance inst in + let subst, ctx = Univ.abstract_universes nas ctx in let args = instance_from_variable_context (List.rev sechyps) in let info = { abstr_ctx = sechyps; diff --git a/vernac/record.ml b/vernac/record.ml index 5b3fb81d66..fb3ef5c09a 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -542,8 +542,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari let univs, ctx_context, fields = match univs with | Polymorphic_const_entry (nas, univs) -> - let () = assert (Int.equal (List.length nas) (Univ.UContext.size univs)) in - let usubst, auctx = Univ.abstract_universes univs in + let usubst, auctx = Univ.abstract_universes nas univs in let usubst = Univ.make_instance_subst usubst in let map c = Vars.subst_univs_level_constr usubst c in let fields = Context.Rel.map map fields in |