diff options
author | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
commit | e4282ea99c664d8d58067bee199cbbcf881b60d5 (patch) | |
tree | d4c4a873eb055c728666f367469fa26c3417793a /contrib/subtac/subtac_obligations.mli | |
parent | a0a94c1340a63cdb824507b973393882666ba52a (diff) |
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'contrib/subtac/subtac_obligations.mli')
-rw-r--r-- | contrib/subtac/subtac_obligations.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 60c0a413..766af2fa 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -21,13 +21,11 @@ val default_tactic : unit -> Proof_type.tactic val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) val get_proofs_transparency : unit -> bool -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 + ?hook:Tacexpr.declaration_hook -> obligation_info -> progress type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list @@ -36,6 +34,7 @@ val add_mutual_definitions : (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> ?tactic:Proof_type.tactic -> ?kind:Decl_kinds.definition_kind -> + ?hook:Tacexpr.declaration_hook -> notations -> Command.fixpoint_kind -> unit |