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, 8 insertions, 6 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index d730d8ef11..9f24fc1587 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -152,7 +152,7 @@ let declare_definition ident (local,k) ce imps hook =
     VarRef ident
   | Discharge | Local | Global ->
     declare_global_definition ident ce local k imps in
-  hook local r
+  Option.default (fun _ r -> r) hook local r
 
 let _ = Obligations.declare_definition_ref := declare_definition
 
@@ -172,7 +172,8 @@ let do_definition ident k bl red_option c ctypopt hook =
       in
       ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      declare_definition ident k ce imps hook
+      ignore(declare_definition ident k ce imps
+        (Option.map (fun f l r -> f l r;r) hook))
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
@@ -530,7 +531,7 @@ let declare_fix kind f def t imps =
     const_entry_opaque = false;
     const_entry_inline_code = false
   } in
-  declare_definition f kind ce imps (fun _ r -> r)
+  declare_definition f kind ce imps None
 
 let _ = Obligations.declare_fix_ref := declare_fix
 
@@ -742,7 +743,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let evars, _, evars_def, evars_typ = 
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
   in
-    ignore(Obligations.add_definition recname ~term:evars_def evars_typ evars ~hook)
+    ignore(Obligations.add_definition
+      recname ~term:evars_def evars_typ evars ~hook:(Some hook))
 
 
 let interp_recursive isfix fixl notations =
@@ -822,7 +824,7 @@ let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
     Lemmas.start_proof_with_initialization (Global,DefinitionBody Fixpoint)
-      (Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
+      (Some(false,indexes,init_tac)) thms None None
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -849,7 +851,7 @@ let declare_cofixpoint local ((fixnames,fixdefs,fixtypes),fiximps) ntns =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
     Lemmas.start_proof_with_initialization (Global,DefinitionBody CoFixpoint)
-      (Some(true,[],init_tac)) thms None (fun _ _ -> ())
+      (Some(true,[],init_tac)) thms None None
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in