diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-03-28 19:24:02 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:45:18 +0200 |
| commit | 44f462aa380de847452c0809d15c86649d5d6a7a (patch) | |
| tree | 840d369425f4b5fc2f6c41fb8dba91e90e8cfbc4 /vernac | |
| parent | 1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff) | |
Extend definition of inductives to include subtyping info
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 2 | ||||
| -rw-r--r-- | vernac/discharge.ml | 9 | ||||
| -rw-r--r-- | vernac/record.ml | 4 | ||||
| -rw-r--r-- | vernac/record.mli | 3 |
4 files changed, 13 insertions, 5 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 998e7803e..5f95a42a3 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -656,7 +656,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = uctx; + mind_entry_universes = (uctx, Univ.UContext.empty); }, pl, impls diff --git a/vernac/discharge.ml b/vernac/discharge.ml index 65ade7887..9c70eb97e 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -86,6 +86,13 @@ let process_inductive (sechyps,abs_ctx) modlist mib = inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) else Univ.Instance.empty, mib.mind_universes in + let substsbt, univssbt = + if mib.mind_polymorphic then + let inst = Univ.UContext.instance mib.mind_subtyping in + let cstrs = Univ.UContext.constraints mib.mind_subtyping in + inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs) + else Univ.Instance.empty, Univ.UContext.empty + in let inds = Array.map_to_list (fun mip -> @@ -116,5 +123,5 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_inds = inds'; mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; - mind_entry_universes = univs; + mind_entry_universes = (univs, univssbt); } diff --git a/vernac/record.ml b/vernac/record.ml index 2400fa681..5c76bb4b2 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -466,7 +466,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure BiFinite poly (ctx, Univ.UContext.empty) (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -571,7 +571,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure finite poly ctx idstruc + let ind = declare_structure finite poly (ctx, Univ.UContext.empty) idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind diff --git a/vernac/record.mli b/vernac/record.mli index 3fd651db9..a380b041a 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -26,7 +26,8 @@ val declare_projections : val declare_structure : Decl_kinds.recursivity_kind -> - bool (** polymorphic?*) -> Univ.universe_context -> + bool (** polymorphic?*) -> + (Univ.universe_context * Univ.universe_context) (** universe and subtyping constraints *) -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) bool (** template arity ? *) -> |