diff options
Diffstat (limited to 'contrib/subtac/subtac_obligations.mli')
| -rw-r--r-- | contrib/subtac/subtac_obligations.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 7d93d57bb8..a8039300a6 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,7 +1,12 @@ open Util -val add_entry : Names.identifier -> Term.constr -> Term.types -> - (Names.identifier * Term.types * Intset.t) array -> unit +type obligation_info = (Names.identifier * Term.types * Intset.t) array + +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 val subtac_obligation : int * Names.identifier option -> unit |