From 76185d638e7a31322a467a3fbd97ac2d30a73bcc Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 26 Aug 2008 15:30:47 +0000
Subject: 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
---
 contrib/subtac/subtac_classes.ml  | 4 ++--
 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
-- 
cgit v1.2.3