diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-26 16:20:41 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-26 16:20:41 +0000 |
| commit | d56e6710b232665fbc5e5199a1c7e51f61d8a6fc (patch) | |
| tree | e242dc39f64b1b56a0862a195c5ef33f00fe6657 | |
| parent | d081dcfaedb5b7e2ad78574a053bcebc4bfb564a (diff) | |
New instance returns the (future) identifier of the instance.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10590 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 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 diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 809888f0d..d8f326698 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 |