diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:38 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:38 +0200 |
| commit | 3a420f4ad929e8372d32c735fd0fd89dfc0346a1 (patch) | |
| tree | 943a01d103c1296dc7c07cb188af994354c4d9a3 /contrib/subtac/subtac_obligations.mli | |
| parent | 1769cbaddea77112dd6f336316d8eb9a0945a1e6 (diff) | |
| parent | e4282ea99c664d8d58067bee199cbbcf881b60d5 (diff) | |
Merge commit 'upstream/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 |