diff options
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 37af8e1f55..bb5ebd7148 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -373,10 +373,10 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t the refinement manually.*) let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in - let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in + let kind = Decl_kinds.Global ImportDefaultBehavior, Decl_kinds.DefinitionBody Decl_kinds.Instance in let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in let info = Lemmas.Info.make ~hook () in - let lemma = Lemmas.start_lemma ~name:id ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in + let lemma = Lemmas.start_lemma ~name:id ~poly ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in (* spiwack: I don't know what to do with the status here. *) let lemma = if not (Option.is_empty term) then |