diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 37ee33b19f..52c1e1cf98 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -9,9 +9,9 @@ (************************************************************************) (*i*) +module CVars = Vars open Names open EConstr -open Nametab open CErrors open Util open Typeclasses_errors @@ -66,7 +66,7 @@ let intern_info {hint_priority;hint_pattern} = (** TODO: add subinstances *) let existing_instance glob g info = - let c = global g in + let c = Nametab.global g in let info = Option.default Hints.empty_hint_info info in let info = intern_info info in let instance, _ = Global.type_of_global_in_context (Global.env ()) c in @@ -116,8 +116,8 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = let kind = IsDefinition Instance in let sigma = - let levels = Univ.LSet.union (Univops.universes_of_constr termtype) - (Univops.universes_of_constr term) in + let levels = Univ.LSet.union (CVars.universes_of_constr termtype) + (CVars.universes_of_constr term) in Evd.restrict_universe_context sigma levels in let uctx = Evd.check_univ_decl ~poly sigma decl in @@ -149,7 +149,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype = let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in if program_mode then - let hook vis gr _ = + let hook _ vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; let pri = intern_info pri in @@ -163,7 +163,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id in obls, Some constr, typ | None -> [||], None, termtype in - let hook = Lemmas.mk_hook hook in + let hook = Obligations.mk_univ_hook hook in let ctx = Evd.evar_universe_context sigma in ignore (Obligations.add_definition id ?term:constr ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls) @@ -425,7 +425,7 @@ let context poly l = | Some b -> let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in - let hook = Lemmas.mk_hook (fun _ gr -> gr) in + let hook = Lemmas.mk_hook (fun _ _ -> ()) in let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in |