diff options
Diffstat (limited to 'contrib/subtac/subtac_obligations.mli')
| -rw-r--r-- | contrib/subtac/subtac_obligations.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 6d13e3bd3a..355ca7cd7d 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,9 +1,10 @@ open Names open Util open Libnames +open Evd -type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array - (* ident, type, location, opaque or transparent, dependencies *) +type obligation_info = (identifier * Term.types * loc * obligation_definition_status * Intset.t) array + (* ident, type, location, opaque or transparent, expand or define dependencies *) type progress = (* Resolution status of a program *) | Remain of int (* n obligations remaining *) @@ -21,6 +22,7 @@ type definition_hook = global_reference -> unit val add_definition : Names.identifier -> Term.constr -> Term.types -> ?implicits:(Topconstr.explicitation * (bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> + ?tactic:Proof_type.tactic -> ?hook:definition_hook -> obligation_info -> progress type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list @@ -28,6 +30,7 @@ type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) val add_mutual_definitions : (Names.identifier * Term.constr * Term.types * (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> + ?tactic:Proof_type.tactic -> ?kind:Decl_kinds.definition_kind -> notations -> Command.fixpoint_kind -> unit |