From 34d85e1e899f8a045659ccc53bfd6a1f5104130b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 17:22:24 +0200 Subject: Use Entries.constant_universes_entry more. This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean. --- vernac/class.ml | 4 ++-- vernac/classes.ml | 34 +++++++++++++------------------- vernac/command.ml | 44 +++++++++++++++++++++++------------------ vernac/declareDef.ml | 4 ++-- vernac/declareDef.mli | 7 +++++-- vernac/lemmas.ml | 36 ++++++++++++++-------------------- vernac/obligations.ml | 17 +++++----------- vernac/record.ml | 54 +++++++++++++++++++++++++++------------------------ 8 files changed, 97 insertions(+), 103 deletions(-) (limited to 'vernac') diff --git a/vernac/class.ml b/vernac/class.ml index 68fd22cb6..943da8fa8 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -212,10 +212,10 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = Evd.to_universe_context sigma in + let univs = Evd.const_univ_entry ~poly sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs + (definition_entry ~types:typ_f ~univs ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in diff --git a/vernac/classes.ml b/vernac/classes.ml index c99eba2cc..1833b7a1d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -119,9 +119,9 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter (Univops.universes_of_constr term) in Evd.restrict_universe_context evm levels in - let uctx = Evd.check_univ_decl evm decl in + let uctx = Evd.check_univ_decl ~poly evm decl in let entry = - Declare.definition_entry ~types:termtype ~poly ~univs:uctx term + Declare.definition_entry ~types:termtype ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in @@ -203,16 +203,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) nf t in Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); - let ctx = Evd.check_univ_decl !evars decl in - let ctx = if poly - then Polymorphic_const_entry ctx - else - (* FIXME be smarter about this *) - Monomorphic_const_entry (Univ.ContextSet.of_context ctx) - in + let univs = Evd.check_univ_decl ~poly !evars decl in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry - (None,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); instance_hook k pri global imps ?hook (ConstRef cst); id @@ -391,19 +385,16 @@ let context poly l = let fn status (id, b, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then (* Declare the universe context once *) - let univs = !uctx in + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) + else Monomorphic_const_entry !uctx + in let () = uctx := Univ.ContextSet.empty in let decl = match b with | None -> - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context univs) - else Monomorphic_const_entry univs - in (ParameterEntry (None,(t,univs),None), IsAssumption Logical) | Some b -> - (* FIXME be smarter about this *) - let univs = Univ.ContextSet.to_context univs in - let entry = Declare.definition_entry ~poly ~univs ~types:t b in + let entry = Declare.definition_entry ~univs ~types:t b in (DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in @@ -426,9 +417,12 @@ let context poly l = pi3 (Command.declare_assumption false decl (t, !uctx) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> - let ctx = Univ.ContextSet.to_context !uctx in + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) + else Monomorphic_const_entry !uctx + in let decl = (Discharge, poly, Definition) in - let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + let entry = Declare.definition_entry ~univs ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () diff --git a/vernac/command.ml b/vernac/command.ml index 06d0c8470..1a8b16a89 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -88,7 +88,7 @@ let warn_implicits_in_term = strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here.") -let interp_definition pl bl p red_option c ctypopt = +let interp_definition pl bl poly red_option c ctypopt = let env = Global.env() in let evd, decl = Univdecls.interp_univ_decl_opt env pl in let evdref = ref evd in @@ -105,15 +105,15 @@ let interp_definition pl bl p red_option c ctypopt = let c = EConstr.Unsafe.to_constr c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = Univops.universes_of_constr body in - let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl evd decl in + let vars = Univops.universes_of_constr body in + let evd = Evd.restrict_universe_context !evdref vars in + let uctx = Evd.check_univ_decl ~poly evd decl in let binders = Evd.universe_binders evd in imps1@(Impargs.lift_implicits nb_args imps2), binders, - definition_entry ~univs:uctx ~poly:p body + definition_entry ~univs:uctx body | Some ctyp -> - let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in - let subst = evd_comb0 Evd.nf_univ_variables evdref in + let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in + let subst = evd_comb0 Evd.nf_univ_variables evdref in let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in @@ -134,10 +134,10 @@ let interp_definition pl bl p red_option c ctypopt = let vars = Univ.LSet.union (Univops.universes_of_constr body) (Univops.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl ctx decl in + let uctx = Evd.check_univ_decl ~poly ctx decl in let binders = Evd.universe_binders evd in imps1@(Impargs.lift_implicits nb_args impsty), binders, - definition_entry ~types:typ ~poly:p + definition_entry ~types:typ ~univs:uctx body in red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps @@ -282,9 +282,14 @@ let do_assumptions_bound_univs coe kind nl id pl c = let ty = nf ty in let vars = Univops.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd decl in let binders = Evd.universe_binders evd in - let uctx = Univ.ContextSet.of_context uctx in + let uctx = match uctx with + | Polymorphic_const_entry uctx -> + (* ?? *) + Univ.ContextSet.of_context uctx + | Monomorphic_const_entry uctx -> uctx + in let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in st @@ -582,7 +587,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in - let uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl ~poly evd decl in List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -604,12 +609,13 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in let univs = - if poly then + match uctx with + | Polymorphic_const_entry uctx -> if cum then Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) else Polymorphic_ind_entry uctx - else - Monomorphic_ind_entry (Univ.ContextSet.of_context uctx) + | Monomorphic_const_entry uctx -> + Monomorphic_ind_entry uctx in (* Build the mutual inductive entry *) let mind_ent = @@ -1032,9 +1038,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in - let univs = Evd.check_univ_decl !evdref decl in + let univs = Evd.check_univ_decl ~poly !evdref decl in (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in + let ce = definition_entry ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in @@ -1173,7 +1179,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl ~poly evd pl in let pl = Evd.universe_binders evd in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) @@ -1206,7 +1212,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl ~poly evd pl in let pl = Evd.universe_binders evd in ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index c18744052..980db4109 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -57,7 +57,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = declare_global_definition ident ce local k pl imps in Lemmas.call_hook fix_exn hook local r -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in +let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = + let ce = definition_entry ~opaque ~types:t ~univs ~eff def in declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 01a87818a..55f7c7861 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -15,5 +15,8 @@ val declare_definition : Id.t -> definition_kind -> Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference -val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.UContext.t -> Id.t -> - Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference +val declare_fix : ?opaque:bool -> definition_kind -> + Universes.universe_binders -> Entries.constant_universes_entry -> + Id.t -> Safe_typing.private_constants Entries.proof_output -> + Constr.types -> Impargs.manual_implicits -> + Globnames.global_reference diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index f59b5fcae..a787ec6fa 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -224,7 +224,7 @@ let compute_proof_name locality = function let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in next_global_ident_away default_thm_id avoid -let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> @@ -232,7 +232,13 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Discharge -> let impl = false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in + let univs = match univs with + | Polymorphic_const_entry univs -> + (* What is going on here? *) + Univ.ContextSet.of_context univs + | Monomorphic_const_entry univs -> univs + in + let c = SectionLocalAssum ((t_i, univs),p,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> @@ -242,11 +248,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Global -> false | Discharge -> assert false in - let ctx = if p - then Polymorphic_const_entry ctx - else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) - in - let decl = (ParameterEntry (None,(t_i,ctx),None), k) in + let decl = (ParameterEntry (None,(t_i,univs),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) | Some body -> @@ -264,8 +266,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im let body_i = body_i body in match locality with | Discharge -> - let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p - ~univs:ctx body_i in + let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in (Discharge,VarRef id,imps) @@ -276,7 +277,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Discharge -> assert false in let const = - Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i + Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality,ConstRef kn,imps) @@ -425,7 +426,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = UState.check_univ_decl ctx decl in + let ctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in @@ -460,7 +461,7 @@ let start_proof_com ?inference_hook kind thms hook = let () = let open Misctypes in if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then - ignore (Evd.check_univ_decl evd decl) + ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl) in let evd = if pi2 kind then evd @@ -495,10 +496,7 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = if pi2 k (* polymorphic *) - then Polymorphic_const_entry (UState.context (fst universes)) - else Monomorphic_const_entry (UState.context_set (fst universes)) - in + let ctx = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> @@ -521,12 +519,8 @@ let save_proof ?proof = function | _ -> None in let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in - let ctx = Evd.check_univ_decl evd decl in let poly = pi2 k in - let ctx = if poly - then Polymorphic_const_entry ctx - else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) - in + let ctx = Evd.check_univ_decl ~poly evd decl in let binders = if poly then Some (UState.universe_binders universes) else None in Admitted(id,k,(sec_vars, (typ, ctx), None), (universes, binders)) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a9110c76c..97cdd7977 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -475,12 +475,8 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in - let ce = - definition_entry ~fix_exn - ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(UState.context prg.prg_ctx) (nf body) - in + let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) prg.prg_ctx prg.prg_univdecl in + let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~univs (nf body) in let () = progmap_remove prg in let ubinders = UState.universe_binders prg.prg_ctx in DeclareDef.declare_definition prg.prg_name @@ -549,9 +545,9 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let ctx = UState.context first.prg_ctx in + let univs = UState.const_univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; @@ -856,10 +852,7 @@ let obligation_terminator name num guard hook auto pf = | (_, status), Vernacexpr.Transparent -> status in let obl = { obl with obl_status = false, status } in - let uctx = if pi2 prg.prg_kind - then Polymorphic_const_entry (UState.context ctx) - else Monomorphic_const_entry (UState.context_set ctx) - in + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in diff --git a/vernac/record.ml b/vernac/record.ml index faf277d86..1d255b08e 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -95,7 +95,7 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields finite def id pl t ps nots fs = +let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env0 = Global.env () in let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in let evars = ref evd in @@ -167,7 +167,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let newps = List.map (EConstr.to_rel_decl evars) newps in let typ = EConstr.to_constr evars typ in let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in - let univs = Evd.check_univ_decl evars decl in + let univs = Evd.check_univ_decl ~poly evars decl in let ubinders = Evd.universe_binders evars in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); @@ -449,7 +449,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params arity +let declare_class finite def cum ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -464,21 +464,21 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params 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 ~poly ~univs:ctx class_body in + 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, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) 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 ~poly - ~univs:(if poly then ctx else Univ.UContext.empty) proj_body - 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 @@ -495,13 +495,14 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params cref, [Name proj_name, sub, Some proj_cst] | _ -> let univs = - if poly then + match univs with + | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) else - Polymorphic_ind_entry ctx - else - Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) + Polymorphic_ind_entry univs + | Monomorphic_const_entry univs -> + Monomorphic_ind_entry univs in let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields @@ -524,13 +525,15 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params params, params in let univs, ctx_context, fields = - if poly then - let usubst, auctx = Univ.abstract_universes ctx in + match univs with + | Polymorphic_const_entry univs -> + let usubst, auctx = Univ.abstract_universes univs 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 - else Univ.AUContext.empty, ctx_context, fields + | Monomorphic_const_entry _ -> + Univ.AUContext.empty, ctx_context, fields in let k = { cl_univs = univs; @@ -606,14 +609,14 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf 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, ctx, arity, template, implpars, params, implfs, fields = + let pl, univs, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> - typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in + typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in let sign = structure_signature (fields@params) in match kind with | Class def -> let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - let gr = declare_class finite def cum poly pl ctx (loc,idstruc) idbuild + let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> @@ -622,13 +625,14 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf (succ (List.length params)) impls) implfs in let univs = - if poly then + match univs with + | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) else - Polymorphic_ind_entry ctx - else - Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) + 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 -- cgit v1.2.3