diff options
| -rw-r--r-- | toplevel/classes.ml | 6 | ||||
| -rw-r--r-- | toplevel/classes.mli | 2 |
2 files changed, 3 insertions, 5 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 627633ad54..1f2253d4f3 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -494,16 +494,14 @@ let new_instance ctx (instid, bk, cl) props = let kn = Declare.declare_constant id cdecl in Flags.if_verbose Command.definition_message id; hook kn; - Some id + id else let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false); Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *) (!refine_ref (evm, term)); Flags.if_verbose (msg $$ Printer.pr_open_subgoals) (); - None - - + id let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 809888f0d7..d8f326698f 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -43,7 +43,7 @@ val new_instance : local_binder list -> typeclass_constraint -> binder_def_list -> - identifier option + identifier val context : typeclass_context -> unit |