diff options
Diffstat (limited to 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 620 |
1 files changed, 620 insertions, 0 deletions
diff --git a/vernac/record.ml b/vernac/record.ml new file mode 100644 index 00000000..78e68e8a --- /dev/null +++ b/vernac/record.ml @@ -0,0 +1,620 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Term +open Sorts +open Util +open Names +open Globnames +open Nameops +open Constr +open Vars +open Environ +open Declarations +open Entries +open Declare +open Constrintern +open Decl_kinds +open Type_errors +open Constrexpr +open Constrexpr_ops +open Goptions +open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration + +(********** definition d'un record (structure) **************) + +(** Flag governing use of primitive projections. Disabled by default. *) +let primitive_flag = ref false +let _ = + declare_bool_option + { optdepr = false; + optname = "use of primitive projections"; + optkey = ["Primitive";"Projections"]; + optread = (fun () -> !primitive_flag) ; + optwrite = (fun b -> primitive_flag := b) } + +let typeclasses_strict = ref false +let _ = + declare_bool_option + { optdepr = false; + optname = "strict typeclass resolution"; + optkey = ["Typeclasses";"Strict";"Resolution"]; + optread = (fun () -> !typeclasses_strict); + optwrite = (fun b -> typeclasses_strict := b); } + +let typeclasses_unique = ref false +let _ = + declare_bool_option + { optdepr = false; + optname = "unique typeclass instances"; + optkey = ["Typeclasses";"Unique";"Instances"]; + optread = (fun () -> !typeclasses_unique); + optwrite = (fun b -> typeclasses_unique := b); } + +let interp_fields_evars env sigma impls_env nots l = + List.fold_left2 + (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) -> + let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in + let sigma, b' = + Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@ + interp_casted_constr_evars_impls env sigma ~impls x t') (sigma,None) b in + let impls = + match i with + | Anonymous -> impls + | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls + in + let d = match b' with + | None -> LocalAssum (i,t') + | Some b' -> LocalDef (i,b',t') + in + List.iter (Metasyntax.set_notation_for_interpretation env impls) no; + (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls)) + (env, sigma, [], [], impls_env) nots l + +let compute_constructor_level evars env l = + List.fold_right (fun d (env, univ) -> + let univ = + if is_local_assum d then + let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in + Univ.sup (univ_of_sort s) univ + else univ + in (EConstr.push_rel d env, univ)) + l (env, Univ.type0m_univ) + +let binder_of_decl = function + | Vernacexpr.AssumExpr(n,t) -> (n,None,t) + | Vernacexpr.DefExpr(n,c,t) -> + (n,Some c, match t with Some c -> c + | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Misctypes.IntroAnonymous, None)) + +let binders_of_decls = List.map binder_of_decl + +let typecheck_params_and_fields finite def id poly pl t ps nots fs = + let env0 = Global.env () in + let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in + let _ = + let error bk {CAst.loc; v=name} = + match bk, name with + | Default _, Anonymous -> + user_err ?loc ~hdr:"record" (str "Record parameters must be named") + | _ -> () + in + List.iter + (function CLocalDef (b, _, _) -> error default_binder_kind b + | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls + | CLocalPattern {CAst.loc} -> + Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps + in + let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in + let sigma, typ, sort, template = match t with + | Some t -> + let env = EConstr.push_rel_context newps env0 in + let poly = + match t with + | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in + let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in + let sred = Reductionops.whd_allnolet env sigma s in + (match EConstr.kind sigma sred with + | Sort s' -> + let s' = EConstr.ESorts.kind sigma s' in + (if poly then + match Evd.is_sort_variable sigma s' with + | Some l -> + let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in + sigma, s, s', true + | None -> + sigma, s, s', false + else sigma, s, s', false) + | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) + | None -> + let uvarkind = Evd.univ_flexible_alg in + let sigma, s = Evd.new_sort_variable uvarkind sigma in + sigma, EConstr.mkSort s, s, true + in + let arity = EConstr.it_mkProd_or_LetIn typ newps in + let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in + let assums = List.filter is_local_assum newps in + let params = List.map (RelDecl.get_name %> Name.get_id) assums in + let ty = Inductive (params,(finite != Declarations.BiFinite)) in + let impls_env = compute_internalization_env env0 sigma ~impls:impls_env ty [id] [arity] [imps] in + let env2,sigma,impls,newfs,data = + interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) + in + let sigma = + Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma Evd.empty in + let sigma, typ = + let _, univ = compute_constructor_level sigma env_ar newfs in + if not def && (Sorts.is_prop sort || + (Sorts.is_set sort && is_impredicative_set env0)) then + sigma, typ + else + let sigma = Evd.set_leq_sort env_ar sigma (Type univ) sort in + if Univ.is_small_univ univ && + Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then + (* We can assume that the level in aritysort is not constrained + and clear it, if it is flexible *) + Evd.set_eq_sort env_ar sigma (Prop Pos) sort, + EConstr.mkSort (Sorts.sort_of_univ univ) + else sigma, typ + in + let sigma, _ = Evarutil.nf_evars_and_universes sigma in + let newfs = List.map (EConstr.to_rel_decl sigma) newfs in + let newps = List.map (EConstr.to_rel_decl sigma) newps in + let typ = EConstr.to_constr sigma typ in + let ce t = Pretyping.check_evars env0 Evd.empty sigma (EConstr.of_constr t) in + let univs = Evd.check_univ_decl ~poly sigma decl in + let ubinders = Evd.universe_binders sigma in + List.iter (iter_constr ce) (List.rev newps); + List.iter (iter_constr ce) (List.rev newfs); + ubinders, univs, typ, template, imps, newps, impls, newfs + +let degenerate_decl decl = + let id = match RelDecl.get_name decl with + | Name id -> id + | Anonymous -> anomaly (Pp.str "Unnamed record variable.") in + match decl with + | LocalAssum (_,t) -> (id, LocalAssumEntry t) + | LocalDef (_,b,_) -> (id, LocalDefEntry b) + +type record_error = + | MissingProj of Id.t * Id.t list + | BadTypedProj of Id.t * env * Type_errors.type_error + +let warn_cannot_define_projection = + CWarnings.create ~name:"cannot-define-projection" ~category:"records" + (fun msg -> hov 0 msg) + +(* If a projection is not definable, we throw an error if the user +asked it to be a coercion. Otherwise, we just print an info +message. The user might still want to name the field of the record. *) +let warning_or_error coe indsp err = + let st = match err with + | MissingProj (fi,projs) -> + let s,have = if List.length projs > 1 then "s","were" else "","was" in + (Id.print fi ++ + strbrk" cannot be defined because the projection" ++ str s ++ spc () ++ + prlist_with_sep pr_comma Id.print projs ++ spc () ++ str have ++ + strbrk " not defined.") + | BadTypedProj (fi,ctx,te) -> + match te with + | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) -> + (Id.print fi ++ + strbrk" cannot be defined because it is informative and " ++ + Printer.pr_inductive (Global.env()) indsp ++ + strbrk " is not.") + | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) -> + (Id.print fi ++ + strbrk" cannot be defined because it is large and " ++ + Printer.pr_inductive (Global.env()) indsp ++ + strbrk " is not.") + | _ -> + (Id.print fi ++ strbrk " cannot be defined because it is not typable.") + in + if coe then user_err ~hdr:"structure" st; + warn_cannot_define_projection (hov 0 st) + +type field_status = + | NoProjection of Name.t + | Projection of constr + +exception NotDefinable of record_error + +(* This replaces previous projection bodies in current projection *) +(* Undefined projs are collected and, at least one undefined proj occurs *) +(* in the body of current projection then the latter can not be defined *) +(* [c] is defined in ctxt [[params;fields]] and [l] is an instance of *) +(* [[fields]] defined in ctxt [[params;x:ind]] *) +let subst_projection fid l c = + let lv = List.length l in + let bad_projs = ref [] in + let rec substrec depth c = match Constr.kind c with + | Rel k -> + (* We are in context [[params;fields;x:ind;...depth...]] *) + if k <= depth+1 then + c + else if k-depth-1 <= lv then + match List.nth l (k-depth-2) with + | Projection t -> lift depth t + | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k + | NoProjection Anonymous -> + user_err (str "Field " ++ Id.print fid ++ + str " depends on the " ++ pr_nth (k-depth-1) ++ str + " field which has no name.") + else + mkRel (k-lv) + | _ -> Constr.map_with_binders succ substrec depth c + in + let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *) + let c'' = substrec 0 c' in + if not (List.is_empty !bad_projs) then + raise (NotDefinable (MissingProj (fid,List.rev !bad_projs))); + c'' + +let instantiate_possibly_recursive_type indu paramdecls fields = + let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in + Termops.substl_rel_context (subst@[mkIndU indu]) fields + +let warn_non_primitive_record = + CWarnings.create ~name:"non-primitive-record" ~category:"record" + (fun (env,indsp) -> + (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ + strbrk" could not be defined as a primitive record"))) + +(* We build projections *) +let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields = + let env = Global.env() in + let (mib,mip) = Global.lookup_inductive indsp in + let poly = Declareops.inductive_is_polymorphic mib in + let u = match ctx with + | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Monomorphic_const_entry ctx -> Univ.Instance.empty + 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 + let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*) + let x = Name binder_name in + let fields = instantiate_possibly_recursive_type indu paramdecls fields in + let lifted_fields = Termops.lift_rel_context 1 fields in + let primitive = + if !primitive_flag then + let is_primitive = + match mib.mind_record with + | Some (Some _) -> true + | Some None | None -> false + in + if not is_primitive then + warn_non_primitive_record (env,indsp); + is_primitive + else false + in + let (_,_,kinds,sp_projs,_) = + List.fold_left3 + (fun (nfi,i,kinds,sp_projs,subst) coe decl impls -> + let fi = RelDecl.get_name decl in + let ti = RelDecl.get_type decl in + let (sp_projs,i,subst) = + match fi with + | Anonymous -> + (None::sp_projs,i,NoProjection fi::subst) + | Name fid -> try + let kn, term = + if is_local_assum decl && primitive then + (** Already defined in the kernel silently *) + let gr = Nametab.locate (Libnames.qualid_of_ident fid) in + let kn = destConstRef gr in + Declare.definition_message fid; + Universes.register_universe_binders gr ubinders; + kn, mkProj (Projection.make kn false,mkRel 1) + else + let ccl = subst_projection fid subst ti in + let body = match decl with + | LocalDef (_,ci,_) -> subst_projection fid subst ci + | LocalAssum _ -> + (* [ccl] is defined in context [params;x:rp] *) + (* [ccl'] is defined in context [params;x:rp;x:rp] *) + let ccl' = liftn 1 2 ccl in + let p = mkLambda (x, lift 1 rp, ccl') in + let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in + let ci = Inductiveops.make_case_info env indsp LetStyle in + mkCase (ci, p, mkRel 1, [|branch|]) + in + let proj = + it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in + let projtyp = + it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in + try + let entry = { + const_entry_body = + Future.from_val (Safe_typing.mk_pure_proof proj); + const_entry_secctx = None; + const_entry_type = Some projtyp; + const_entry_universes = ctx; + const_entry_opaque = false; + const_entry_inline_code = false; + const_entry_feedback = None } in + let k = (DefinitionEntry entry,IsDefinition kind) in + let kn = declare_constant ~internal:InternalTacticRequest fid k in + let constr_fip = + let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in + applist (mkConstU (kn,u),proj_args) + in + Declare.definition_message fid; + Universes.register_universe_binders (ConstRef kn) ubinders; + kn, constr_fip + with Type_errors.TypeError (ctx,te) -> + raise (NotDefinable (BadTypedProj (fid,ctx,te))) + in + let refi = ConstRef kn in + Impargs.maybe_declare_manual_implicits false refi impls; + if coe then begin + let cl = Class.class_of_global (IndRef indsp) in + Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl + end; + let i = if is_local_assum decl then i+1 else i in + (Some kn::sp_projs, i, Projection term::subst) + with NotDefinable why -> + warning_or_error coe indsp why; + (None::sp_projs,i,NoProjection fi::subst) in + (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst)) + (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) + in (kinds,sp_projs) + +open Typeclasses + +let declare_structure finite ubinders univs id idbuild paramimpls params arity template + fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers = + let nparams = List.length params and nfields = List.length fields in + let args = Context.Rel.to_extended_list mkRel nfields params in + let ind = applist (mkRel (1+nparams+nfields), args) in + let type_constructor = it_mkProd_or_LetIn ind fields in + let template, ctx = + match univs with + | Monomorphic_ind_entry ctx -> + template, Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry ctx -> + false, Polymorphic_const_entry ctx + | Cumulative_ind_entry cumi -> + false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi) + in + let binder_name = + match name with + | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) + | Some n -> n + in + let mie_ind = + { mind_entry_typename = id; + mind_entry_arity = arity; + mind_entry_template = template; + mind_entry_consnames = [idbuild]; + mind_entry_lc = [type_constructor] } + in + let mie = + { mind_entry_params = List.map degenerate_decl params; + mind_entry_record = Some (if !primitive_flag then Some binder_name else None); + mind_entry_finite = finite; + mind_entry_inds = [mie_ind]; + mind_entry_private = None; + mind_entry_universes = univs; + } + in + let mie = InferCumulativity.infer_inductive (Global.env ()) mie in + let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in + let rsp = (kn,0) in (* This is ind path of idstruc *) + let cstr = (rsp,1) in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in + let build = ConstructRef cstr in + let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in + let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in + Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); + rsp + +let implicits_of_context ctx = + List.map_i (fun i name -> + let explname = + match name with + | Name n -> Some n + | Anonymous -> None + in ExplByPos (i, explname), (true, true, true)) + 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) + +let declare_class finite def cum ubinders univs id idbuild paramimpls params arity + template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities = + let fieldimpls = + (* Make the class implicit in the projections, and the params if applicable. *) + let len = List.length params in + let impls = implicits_of_context params in + List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls + in + let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in + let impl, projs = + match fields with + | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def -> + let class_body = it_mkLambda_or_LetIn field params in + let class_type = it_mkProd_or_LetIn arity params in + let class_entry = + Declare.definition_entry ~types:class_type ~univs class_body in + let cst = Declare.declare_constant (snd id) + (DefinitionEntry class_entry, IsDefinition Definition) + in + let cstu = (cst, match univs with + | Polymorphic_const_entry univs -> Univ.UContext.instance univs + | Monomorphic_const_entry _ -> Univ.Instance.empty) + in + let inst_type = appvectc (mkConstU cstu) + (Termops.rel_vect 0 (List.length params)) in + let proj_type = + it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in + let proj_body = + it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in + let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in + let proj_cst = Declare.declare_constant proj_name + (DefinitionEntry proj_entry, IsDefinition Definition) + in + let cref = ConstRef cst in + Impargs.declare_manual_implicits false cref [paramimpls]; + Universes.register_universe_binders cref ubinders; + Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; + Universes.register_universe_binders (ConstRef proj_cst) ubinders; + Classes.set_typeclass_transparency (EvalConstRef cst) false false; + let sub = match List.hd coers with + | Some b -> Some ((if b then Backward else Forward), List.hd priorities) + | None -> None + in + cref, [Name proj_name, sub, Some proj_cst] + | _ -> + let univs = + match univs with + | Polymorphic_const_entry univs -> + if cum then + Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs) + else + Polymorphic_ind_entry univs + | Monomorphic_const_entry univs -> + Monomorphic_ind_entry univs + in + let ind = declare_structure Declarations.BiFinite ubinders univs (snd id) idbuild paramimpls + params arity template fieldimpls fields + ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) + in + let coers = List.map2 (fun coe pri -> + Option.map (fun b -> + if b then Backward, pri else Forward, pri) coe) + coers priorities + in + let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y) + (List.rev fields) coers (Recordops.lookup_projections ind) + in IndRef ind, l + in + let ctx_context = + List.map (fun decl -> + match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with + | Some (_, ((cl,_), _)) -> Some cl.cl_impl + | None -> None) + params, params + in + let univs, ctx_context, fields = + match univs with + | Polymorphic_const_entry univs -> + let usubst, auctx = Univ.abstract_universes 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 + let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in + auctx, ctx_context, fields + | Monomorphic_const_entry _ -> + Univ.AUContext.empty, ctx_context, fields + in + let k = + { cl_univs = univs; + cl_impl = impl; + cl_strict = !typeclasses_strict; + cl_unique = !typeclasses_unique; + cl_context = ctx_context; + cl_props = fields; + cl_projs = projs } + in + add_class k; impl + + +let add_constant_class cst = + let ty, univs = Global.type_of_global_in_context (Global.env ()) (ConstRef cst) in + let ctx, arity = decompose_prod_assum ty in + let tc = + { cl_univs = univs; + cl_impl = ConstRef cst; + cl_context = (List.map (const None) ctx, ctx); + cl_props = [LocalAssum (Anonymous, arity)]; + cl_projs = []; + cl_strict = !typeclasses_strict; + cl_unique = !typeclasses_unique + } + in add_class tc; + set_typeclass_transparency (EvalConstRef cst) false false + +let add_inductive_class ind = + let mind, oneind = Global.lookup_inductive ind in + let k = + let ctx = oneind.mind_arity_ctxt in + let univs = Declareops.inductive_polymorphic_context mind in + let env = push_context ~strict:false (Univ.AUContext.repr univs) (Global.env ()) in + let env = push_rel_context ctx env in + let inst = Univ.make_abstract_instance univs in + let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in + { cl_univs = univs; + cl_impl = IndRef ind; + cl_context = List.map (const None) ctx, ctx; + cl_props = [LocalAssum (Anonymous, ty)]; + cl_projs = []; + cl_strict = !typeclasses_strict; + cl_unique = !typeclasses_unique } + in add_class k + +let declare_existing_class g = + match g with + | ConstRef x -> add_constant_class x + | IndRef x -> add_inductive_class x + | _ -> user_err ~hdr:"declare_existing_class" + (Pp.str"Unsupported class type, only constants and inductives are allowed") + +open Vernacexpr + +(* [fs] corresponds to fields and [ps] to parameters; [coers] is a + list telling if the corresponding fields must me declared as coercions + or subinstances. *) +let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl)),ps,cfs,idbuild,s) = + let cfs,notations = List.split cfs in + let cfs,priorities = List.split cfs in + let coers,fs = List.split cfs in + let extract_name acc = function + Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc + | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc + | _ -> acc in + let allnames = idstruc::(List.fold_left extract_name [] fs) in + let () = match List.duplicates Id.equal allnames with + | [] -> () + | id :: _ -> user_err (str "Two objects have the same name" ++ spc () ++ quote (Id.print id)) + in + let isnot_class = match kind with Class false -> false | _ -> true in + if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then + user_err Pp.(str "Priorities only allowed for type class substructures"); + (* Now, younger decl in params and fields is on top *) + let pl, univs, arity, template, implpars, params, implfs, fields = + States.with_state_protection (fun () -> + typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in + match kind with + | Class def -> + let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in + declare_class finite def cum pl univs (loc,idstruc) idbuild + implpars params arity template implfs fields is_coe coers priorities + | _ -> + let implfs = List.map + (fun impls -> implpars @ Impargs.lift_implicits + (succ (List.length params)) impls) implfs + in + let univs = + match univs with + | Polymorphic_const_entry univs -> + if cum then + Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs) + else + Polymorphic_ind_entry univs + | Monomorphic_const_entry univs -> + Monomorphic_ind_entry univs + in + let ind = declare_structure finite pl univs idstruc + idbuild implpars params arity template implfs + fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) in + IndRef ind |