aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-11 17:54:52 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-13 15:14:45 +0200
commit8b3978baa5ceb41aaec4d9864c878847b82682d7 (patch)
tree55743b315a46d9fab7ad6cba6d6bb6a622750de9
parent8f13a227f8d73b78128d9a3bb060cf03d382b708 (diff)
Getting rid of AUContext abstraction breakers in Record.
-rw-r--r--vernac/record.ml21
1 files changed, 10 insertions, 11 deletions
diff --git a/vernac/record.ml b/vernac/record.ml
index 366f50454..b17961648 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -265,16 +265,10 @@ let warn_non_primitive_record =
let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
- let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
- let paramdecls = Inductive.inductive_paramdecls (mib, u) in
let poly = Declareops.inductive_is_polymorphic mib in
- let ctx =
- match mib.mind_universes with
- | Monomorphic_ind ctx -> ctx
- | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
- | Cumulative_ind cumi ->
- Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
- in
+ let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in
+ let u = Univ.UContext.instance ctx in
+ let paramdecls = Inductive.inductive_paramdecls (mib, u) in
let indu = indsp, u in
let r = mkIndU (indsp,u) in
let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
@@ -334,8 +328,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
const_entry_secctx = None;
const_entry_type = Some projtyp;
const_entry_polymorphic = poly;
- const_entry_universes =
- if poly then ctx else Univ.UContext.empty;
+ const_entry_universes = ctx;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None } in
@@ -431,6 +424,12 @@ let declare_structure finite univs id idbuild paramimpls params arity template
let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
+ let fields =
+ if poly then
+ let subst, _ = Univ.abstract_universes ctx in
+ Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields
+ else fields
+ in
let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in
let build = ConstructRef cstr in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in