diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2013-11-27 17:41:31 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2013-12-04 14:14:33 +0100 |
| commit | eaa9c147f1801c363635a5be4e0258e0de1ab02e (patch) | |
| tree | 642acf881a2ff2e980d0001f9ed01ae79554191a /proofs/proof_global.mli | |
| parent | 358a68a90416facf4f149c98332e8118971d4793 (diff) | |
Refactoring: storing more information in the terminator closure.
We used to keep a lot of information in the global proof environment, for the end-of-proof commands to use. Now that the end commands are dumb, they are better stored in the proof-termination closure allocated by the starting command.
In this commit, we remove the compute_guard parameter.
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index eb7d0ecb1..71d03438b 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -56,7 +56,6 @@ type lemma_possible_guards = int list list type proof_object = { id : Names.Id.t; entries : Entries.definition_entry list; - do_guard : lemma_possible_guards; persistence : Decl_kinds.goal_kind; hook : unit Tacexpr.declaration_hook Ephemeron.key } @@ -74,7 +73,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 -> - ?compute_guard:lemma_possible_guards -> unit Tacexpr.declaration_hook -> proof_terminator -> unit @@ -83,7 +81,6 @@ val start_proof : Names.Id.t -> val start_dependent_proof : Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope -> - ?compute_guard:lemma_possible_guards -> unit Tacexpr.declaration_hook -> proof_terminator -> unit |