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

1 files changed, 4 insertions, 4 deletions

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 *)