From c81254903e1e50a2305cd48ccfb673d9737afc48 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 8 Aug 2013 18:52:52 +0000 Subject: get rid of closures in global/proof state In some cases, an 'a -> 'b field is changed into an ('a -> b') option field so that one can forget the closures and marshal the resulting state git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16683 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/lemmas.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'toplevel/lemmas.ml') diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 6876483a0..846714db7 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -183,7 +183,7 @@ let save ?proof id const do_guard (locality,kind) hook = (* if the proof is given explicitly, nothing has to be deleted *) if proof = None then Pfedit.delete_current_proof (); definition_message id; - hook l r + Option.iter (fun f -> f l r) hook let default_thm_id = Id.of_string "Unnamed_thm" @@ -341,8 +341,8 @@ let start_proof_with_initialization kind recguard thms snl hook = let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; - hook strength ref) thms_data in - start_proof id kind t ?init_tac hook ~compute_guard:guard + Option.iter (fun f -> f strength ref) hook) thms_data in + start_proof id kind t ?init_tac (Some hook) ~compute_guard:guard let start_proof_com kind thms hook = let evdref = ref Evd.empty in @@ -368,7 +368,7 @@ let admit () = let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in Pfedit.delete_current_proof (); assumption_message id; - hook Global (ConstRef kn) + Option.iter (fun f -> f Global (ConstRef kn)) hook (* Miscellaneous *) -- cgit v1.2.3