diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index fbcd1744a8..01fc120af2 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -315,7 +315,7 @@ let instance_hook info global imps ?hook cst = let declare_instance_constant info global imps ?hook id decl poly sigma term termtype = (* XXX: Duplication of the declare_constant path *) - let kind = IsDefinition Instance in + let kind = Decls.(IsDefinition Instance) in let sigma = let levels = Univ.LSet.union (CVars.universes_of_constr termtype) (CVars.universes_of_constr term) in @@ -338,7 +338,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in let cst = Declare.declare_constant id - (Declare.ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in + (Declare.ParameterEntry entry, Decls.(IsAssumption Logical)) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook pri global imps (ConstRef cst) @@ -363,7 +363,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt let hook = DeclareDef.Hook.make hook in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition ~name:id ?term:constr - ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls) + ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Decls.Instance ~hook typ ctx obls) let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do @@ -373,7 +373,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in let scope = DeclareDef.Global Declare.ImportDefaultBehavior in - let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in + let kind = Decls.(DefinitionBody Instance) in let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in let info = Lemmas.Info.make ~hook ~scope ~kind () in let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in |