diff options
| author | Arnaud Spiwack | 2013-11-27 17:41:31 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-12-04 14:14:33 +0100 |
| commit | eaa9c147f1801c363635a5be4e0258e0de1ab02e (patch) | |
| tree | 642acf881a2ff2e980d0001f9ed01ae79554191a /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/lemmas.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index db479615ef..9d7a58ff0a 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -299,8 +299,8 @@ let start_hook = ref ignore let set_start_hook = (:=) start_hook -let get_proof proof opacity = - let (id,(const,do_guard,persistence,hook)) = +let get_proof proof do_guard opacity = + let (id,(const,persistence,hook)) = Pfedit.cook_this_proof !save_hook proof in id,{const with const_entry_opaque = opacity},do_guard,persistence,hook @@ -311,7 +311,7 @@ let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook = admit (); Pp.feedback Interface.AddedAxiom | Proved (is_opaque,idopt),proof -> - let proof = get_proof proof is_opaque in + let proof = get_proof proof compute_guard is_opaque in begin match idopt with | None -> save_named proof | Some ((_,id),None) -> save_anonymous proof id @@ -325,7 +325,7 @@ let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook = | None -> initialize_named_context_for_proof () in !start_hook c; - Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook terminator + Pfedit.start_proof id kind sign c ?init_tac hook terminator let rec_tac_initializer finite guard thms snl = |