diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2013-11-27 18:41:09 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2013-12-04 14:14:33 +0100 |
| commit | f1a2c15b7a7d7edfd4b4b379ed0bde8b1f5deb7b (patch) | |
| tree | 7f29564ddfa4d1bf2d4a06b6dd212cc3ef3beaff /proofs/proof_global.mli | |
| parent | eaa9c147f1801c363635a5be4e0258e0de1ab02e (diff) | |
Factoring(continued).
This commit removes the hook.
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 71d03438b..ed7668d57 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -57,7 +57,6 @@ type proof_object = { id : Names.Id.t; entries : Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - hook : unit Tacexpr.declaration_hook Ephemeron.key } type proof_ending = Vernacexpr.proof_end * proof_object @@ -73,7 +72,6 @@ type closed_proof = proof_object*proof_terminator Ephemeron.key val start_proof : Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> - unit Tacexpr.declaration_hook -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between @@ -81,7 +79,6 @@ val start_proof : Names.Id.t -> val start_dependent_proof : Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope -> - unit Tacexpr.declaration_hook -> proof_terminator -> unit @@ -177,7 +174,7 @@ val get_default_goal_selector : unit -> Vernacexpr.goal_selector module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * - Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key) + Decl_kinds.goal_kind) end type state |