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

8 files changed, 31 insertions, 28 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index f9ce75bba7..89cf116ca7 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -297,7 +297,7 @@ let try_add_new_identity_coercion id ~local ~source ~target =
 let try_add_new_coercion_with_source ref ~local ~source =
   try_add_new_coercion_core ref ~local (Some source) None false
 
-let add_coercion_hook local ref =
+let add_coercion_hook = Some (fun local ref ->
   let stre = match local with
   | Local -> true
   | Global -> false
@@ -305,13 +305,13 @@ let add_coercion_hook local ref =
   in
   let () = try_add_new_coercion ref stre in
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
-  Flags.if_verbose msg_info msg
+  Flags.if_verbose msg_info msg)
 
-let add_subclass_hook local ref =
+let add_subclass_hook = Some (fun local ref ->
   let stre = match local with
   | Local -> true
   | Global -> false
   | Discharge -> assert false
   in
   let cl = class_of_global ref in
-  try_add_new_coercion_subclass cl stre
+  try_add_new_coercion_subclass cl stre)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index a217abbba0..fa5d405e21 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -292,13 +292,13 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 		| None -> [||], None, termtype
 	      in
 		ignore (Obligations.add_definition id ?term:constr
-			typ ~kind:(Global,Instance) ~hook obls);
+			typ ~kind:(Global,Instance) ~hook:(Some hook) obls);
 		id
 	    else
 	      (Flags.silently 
 	       (fun () ->
 		Lemmas.start_proof id kind termtype
-		(fun _ -> instance_hook k pri global imps ?hook);
+		(Some (fun _ -> instance_hook k pri global imps ?hook));
 		if not (Option.is_empty term) then 
 		  Pfedit.by (!refine_ref (evm, Option.get term))
 		else if Flags.is_auto_intros () then
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
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 76a3c58027..fe6a0a4003 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -35,7 +35,8 @@ val interp_definition :
   constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
 
 val declare_definition : Id.t -> definition_kind ->
-  definition_entry -> Impargs.manual_implicits -> 'a declaration_hook -> 'a
+  definition_entry -> Impargs.manual_implicits ->
+    Globnames.global_reference declaration_hook -> Globnames.global_reference
 
 val do_definition : Id.t -> definition_kind ->
   local_binder list -> red_expr option -> constr_expr ->
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 6876483a05..846714db7a 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 *)
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 9e7ddd5a66..58201a5f82 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -511,7 +511,7 @@ let declare_definition prg =
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
-      (fun local gr -> prg.prg_hook local gr; gr)
+      (Option.map (fun f l r -> f l r;r) prg.prg_hook)
 
 open Pp
 
@@ -579,7 +579,7 @@ let declare_mutual_definition l =
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
-      first.prg_hook (fst first.prg_kind) gr;
+      Option.iter (fun f -> f (fst first.prg_kind) gr) first.prg_hook;
       List.iter progmap_remove l; kn
 
 let shrink_body c = 
@@ -771,7 +771,7 @@ let rec solve_obligation prg num tac =
       | [] ->
 	  let obl = subst_deps_obl obls obl in
 	    Lemmas.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
-	      (fun strength gr ->
+	      (Some (fun strength gr ->
 		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
 		let obl =
 		  let transparent = evaluable_constant cst (Global.env ()) in
@@ -801,11 +801,11 @@ let rec solve_obligation prg num tac =
 		      let deps = dependencies obls num in
 			if not (Int.Set.is_empty deps) then
 			  ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
-		  | _ -> ());
+		  | _ -> ()));
 	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		     Printer.pr_constr_env (Global.env ()) obl.obl_type);
 	    Pfedit.by (snd (get_default_tactic ()));
-	    Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac
+	    Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
       | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
 		      ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
 
@@ -923,7 +923,7 @@ let show_term n =
 	    ++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
 
 let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
+    ?(reduce=reduce) ?(hook=None) obls =
   let info = str (Id.to_string n) ++ str " has type-checked" in
   let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
@@ -941,7 +941,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
 	| _ -> res)
 
 let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
-    ?(hook=fun _ _ -> ()) notations fixkind =
+    ?(hook=None) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index ddc99a96cb..081871fce5 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -74,7 +74,7 @@ val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:Proof_type.tactic ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:(unit Tacexpr.declaration_hook) -> obligation_info -> progress
+  ?hook:unit Tacexpr.declaration_hook -> obligation_info -> progress
 
 type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5316e9d467..bc74c72115 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -414,11 +414,11 @@ let start_proof_and_print k l hook =
   start_proof_com k l hook;
   print_subgoals ()
 
-let no_hook _ _ = ()
+let no_hook = None
 
 let vernac_definition_hook = function
 | Coercion -> Class.add_coercion_hook
-| CanonicalStructure -> fun _ -> Recordops.declare_canonical_structure
+| CanonicalStructure -> Some (fun _ -> Recordops.declare_canonical_structure)
 | SubClass -> Class.add_subclass_hook
 | _ -> no_hook
 
@@ -797,7 +797,7 @@ let vernac_set_end_tac tac =
     error "Unknown command of the non proof-editing mode.";
   match tac with
   | Tacexpr.TacId [] -> ()
-  | _ -> set_end_tac (Tacinterp.interp tac)
+  | _ -> set_end_tac tac
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
 let vernac_set_used_variables l =