declaration_hooks use Ephemeron

Ideally, any component of the global state that is a function or any
other unmarshallable data should be stocked as an ephemeron to make
the state always marshallable.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16893 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 25 insertions, 25 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 89cf116ca..f9ce75bba 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 = Some (fun local ref ->
+let add_coercion_hook local ref =
   let stre = match local with
   | Local -> true
   | Global -> false
@@ -305,13 +305,13 @@ let add_coercion_hook = Some (fun 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 = Some (fun local ref ->
+let add_subclass_hook 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 fa5d405e2..c460e291c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -117,7 +117,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
 
 let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
     ?(generalize=true)
-    ?(tac:Proof_type.tactic option) ?(hook:(global_reference -> unit) option) pri =
+    ?(tac:Proof_type.tactic option) ?hook pri =
   let env = Global.env() in
   let evars = ref Evd.empty in
   let tclass, ids =
@@ -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:(Some hook) obls);
+			typ ~kind:(Global,Instance) ~hook obls);
 		id
 	    else
 	      (Flags.silently 
 	       (fun () ->
 		Lemmas.start_proof id kind termtype
-		(Some (fun _ -> instance_hook k pri global imps ?hook));
+		(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 9efe4eefc..1dbdcf78c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -151,7 +151,7 @@ let declare_definition ident (local,k) ce imps hook =
     VarRef ident
   | Discharge | Local | Global ->
     declare_global_definition ident ce local k imps in
-  Option.default (fun _ r -> r) hook local r
+  hook local r
 
 let _ = Obligations.declare_definition_ref := declare_definition
 
@@ -172,7 +172,7 @@ let do_definition ident k bl red_option c ctypopt hook =
       ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
       ignore(declare_definition ident k ce imps
-        (Option.map (fun f l r -> f l r;r) hook))
+        (fun l r -> hook l r;r))
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
@@ -530,7 +530,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 None
+  declare_definition f kind ce imps (fun _ r -> r)
 
 let _ = Obligations.declare_fix_ref := declare_fix
 
@@ -743,7 +743,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
   in
     ignore(Obligations.add_definition
-      recname ~term:evars_def evars_typ evars ~hook:(Some hook))
+      recname ~term:evars_def evars_typ evars ~hook)
 
 
 let interp_recursive isfix fixl notations =
@@ -823,7 +823,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 None
+      (Some(false,indexes,init_tac)) thms None (fun _ _ -> ())
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -850,7 +850,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 None
+      (Some(true,[],init_tac)) thms None (fun _ _ -> ())
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 5a936e623..a25f96d46 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -182,7 +182,7 @@ let save ?proof id const do_guard (locality,kind) hook =
   (* if the proof is given explicitly, nothing has to be deleted *)
   if Option.is_empty proof then Pfedit.delete_current_proof ();
   definition_message id;
-  Option.iter (fun f -> f l r) hook
+  Ephemeron.iter_opt hook (fun f -> f l r)
 
 let default_thm_id = Id.of_string "Unnamed_thm"
 
@@ -340,8 +340,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;
-	  Option.iter (fun f -> f strength ref) hook) thms_data in
-      start_proof id kind t ?init_tac (Some hook) ~compute_guard:guard
+	  hook strength ref) thms_data in
+      start_proof id kind t ?init_tac hook ~compute_guard:guard
 
 let start_proof_com kind thms hook =
   let evdref = ref Evd.empty in
@@ -373,7 +373,7 @@ let admit () =
       str "declared as an axiom.")
   in
   let () = assumption_message id in
-  Option.iter (fun f -> f Global (ConstRef kn)) hook
+  Ephemeron.iter_opt hook (fun f -> f Global (ConstRef kn))
 
 (* Miscellaneous *)
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 8c7414568..3c4b88f46 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -517,7 +517,7 @@ let declare_definition prg =
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
-      (Option.map (fun f l r -> f l r;r) prg.prg_hook)
+      (fun l r -> prg.prg_hook l r; r)
 
 open Pp
 
@@ -585,7 +585,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
-      Option.iter (fun f -> f (fst first.prg_kind) gr) first.prg_hook;
+      first.prg_hook (fst first.prg_kind) gr;
       List.iter progmap_remove l; kn
 
 let shrink_body c = 
@@ -777,7 +777,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
-	      (Some (fun strength gr ->
+	      (fun strength gr ->
 		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
 		let obl =
 		  let transparent = evaluable_constant cst (Global.env ()) in
@@ -807,7 +807,7 @@ 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 ()));
@@ -929,7 +929,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=None) obls =
+    ?(reduce=reduce) ?(hook=fun _ _ -> ()) 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
@@ -947,7 +947,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=None) notations fixkind =
+    ?(hook=fun _ _ -> ()) 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/vernacentries.ml b/toplevel/vernacentries.ml
index d63ef9ec1..eb4038721 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 = None
+let no_hook _ _ = ()
 
 let vernac_definition_hook = function
 | Coercion -> Class.add_coercion_hook
-| CanonicalStructure -> Some (fun _ -> Recordops.declare_canonical_structure)
+| CanonicalStructure -> (fun _ -> Recordops.declare_canonical_structure)
 | SubClass -> Class.add_subclass_hook
 | _ -> no_hook