diff options
| author | msozeau | 2008-08-26 15:30:47 +0000 |
|---|---|---|
| committer | msozeau | 2008-08-26 15:30:47 +0000 |
| commit | 76185d638e7a31322a467a3fbd97ac2d30a73bcc (patch) | |
| tree | 9bcfbfe173b7101b28f4a95e809c611f1df2f611 | |
| parent | a87e69e18672ce49a5bc409a7b05cdb70116b698 (diff) | |
Give back progress information after feeding the Program Instance to the
obligation handler.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11335 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_classes.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index efb99bdb0b..9126af23dc 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -191,5 +191,5 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class in let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in - ignore(Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls); - id + id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls + diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli index 1cb03385bb..f2522589f4 100644 --- a/contrib/subtac/subtac_classes.mli +++ b/contrib/subtac/subtac_classes.mli @@ -39,4 +39,4 @@ val new_instance : binder_def_list -> ?on_free_vars:(identifier list -> unit) -> int option -> - identifier + identifier * Subtac_obligations.progress |