diff options
Diffstat (limited to 'contrib/subtac/subtac_obligations.mli')
| -rw-r--r-- | contrib/subtac/subtac_obligations.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index a8039300a6..6ba479764f 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -6,7 +6,7 @@ val add_definition : Names.identifier -> Term.constr -> Term.types -> obligation_info -> unit val add_mutual_definitions : - (Names.identifier * Term.constr * Term.types * obligation_info) list -> unit + (Names.identifier * int * Term.constr * Term.types * obligation_info) list -> unit val subtac_obligation : int * Names.identifier option -> unit |