diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 627633ad5..1f2253d4f 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 |