diff options
| -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 |