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

19 files changed, 55 insertions, 55 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 435064b998..df4ed2c41e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -283,4 +283,4 @@ type raw_tactic_arg =
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
 type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
 
-type 'a declaration_hook = (locality -> global_reference -> 'a) option
+type 'a declaration_hook = locality -> global_reference -> 'a
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index d249df5787..13816d1db7 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -982,7 +982,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     (mk_equation_id f_id)
     (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
     lemma_type
-    None;
+    (fun _ _ -> ());
   Pfedit.by (prove_replacement);
   Lemmas.save_named false
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d11e810e13..58f43ed49e 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -329,7 +329,7 @@ let generate_functional_principle
 	  id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
   in
   let names = ref [new_princ_name] in
-  let hook new_principle_type = Some (fun _ _ ->
+  let hook new_principle_type _ _ =
     if Option.is_empty sorts
     then
       (*     let id_of_f = Label.to_id (con_label f) in *)
@@ -357,7 +357,7 @@ let generate_functional_principle
 	names := name :: !names
       in
       register_with_sort InProp;
-      register_with_sort InSet)
+      register_with_sort InSet
   in
   let (id,(entry,g_kind,hook)) =
     build_functional_principle interactive_proof old_princ_type new_sorts funs i
@@ -519,7 +519,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	this_block_funs
 	0
 	(prove_princ_for_struct false 0 (Array.of_list funs))
-	(fun _ -> None)
+	(fun _ _ _ -> ())
   with e when Errors.noncritical e ->
     begin
       begin
@@ -593,7 +593,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 		 this_block_funs
 		 !i
 		 (prove_princ_for_struct false !i (Array.of_list funs))
-		 (fun _ -> None)
+		 (fun _ _ _ -> ())
 	     in
 	     const
 	 with Found_type i ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e042240e2d..34b3728603 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -352,7 +352,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in 
 	Command.do_definition fname (Decl_kinds.Global,Decl_kinds.Definition)
-	  bl None body (Some ret_type) None
+	  bl None body (Some ret_type) (fun _ _ -> ())
     | _ ->
 	Command.do_fixpoint Global fixpoint_exprl
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f504b0734f..04cc139c01 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -161,7 +161,7 @@ let save with_clean id const (locality,kind) hook =
 	(locality, ConstRef kn)
   in
   if with_clean then  Pfedit.delete_current_proof ();
-  Option.default (fun _ _ -> ()) hook l r;
+  Ephemeron.iter_opt hook (fun f -> f l r);
   definition_message id
 
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 6f47e22893..722f857b34 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -53,7 +53,7 @@ val jmeq_refl : unit -> Term.constr
 val new_save_named : bool -> unit
 
 val save : bool -> Id.t ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
-  unit Tacexpr.declaration_hook -> unit
+  unit Tacexpr.declaration_hook Ephemeron.key -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
    abort the proof
@@ -61,7 +61,7 @@ val save : bool -> Id.t ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
 val get_proof_clean : bool ->
   Names.Id.t *
     (Entries.definition_entry * Decl_kinds.goal_kind *
-      unit Tacexpr.declaration_hook)
+      unit Tacexpr.declaration_hook Ephemeron.key)
 
 
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index bba8564faa..b6a8fdc1a3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1061,7 +1061,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
-           None;
+           (fun _ _ -> ());
 	 Pfedit.by
 	   (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
 	      (proving_tac i));
@@ -1112,7 +1112,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
 	   (fst lemmas_types_infos.(i))
-           None;
+           (fun _ _ -> ());
 	 Pfedit.by
 	   (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
 	      (proving_tac i));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 49a90e432a..22e82035b4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1313,7 +1313,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma)
     sign
     gls_type
-    (Some hook) ;
+    hook;
   if Indfun_common.is_strict_tcc  ()
   then
     by (tclIDTAC)
@@ -1406,7 +1406,7 @@ let (com_eqn : int -> Id.t ->
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (start_proof eq_name (Global, Proof Lemma)
-       (Environ.named_context_val env) equation_lemma_type None;
+       (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
      by
        (start_equation f_ref terminate_ref
 	  (fun  x ->
@@ -1523,6 +1523,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       term_id
       using_lemmas
       (List.length res_vars)
-      (Some hook))
+      hook)
     ()
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a44b3bef3a..2b09470752 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -43,7 +43,8 @@ let cook_this_proof hook p =
   | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
   | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
-let cook_proof hook = cook_this_proof hook (Proof_global.close_proof ())
+let cook_proof hook =
+  cook_this_proof hook (Proof_global.close_proof (fun x -> x))
 let get_pftreestate () =
   Proof_global.give_me_the_proof ()
 
@@ -116,7 +117,7 @@ open Decl_kinds
 let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac =
-  start_proof id goal_kind sign typ None;
+  start_proof id goal_kind sign typ (fun _ _ -> ());
   try
     by tac;
     let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 79929fd8d5..7df0da8003 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -75,15 +75,15 @@ val cook_this_proof : (Proof.proof -> unit) ->
     (Entries.definition_entry list *
     lemma_possible_guards *
     Decl_kinds.goal_kind *
-    unit Tacexpr.declaration_hook) ->
+    unit Tacexpr.declaration_hook Ephemeron.key) ->
   Id.t *
     (Entries.definition_entry * lemma_possible_guards * goal_kind *
-     unit declaration_hook)
+     unit declaration_hook Ephemeron.key)
 
 val cook_proof : (Proof.proof -> unit) ->
   Id.t *
     (Entries.definition_entry * lemma_possible_guards * goal_kind *
-     unit declaration_hook)
+     unit declaration_hook Ephemeron.key)
 
 (** {6 ... } *)
 (** [get_pftreestate ()] returns the current focused pending proof.
@@ -104,7 +104,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env
 (** [current_proof_statement] *)
 
 val current_proof_statement :
-  unit -> Id.t * goal_kind * types * unit declaration_hook
+  unit -> Id.t * goal_kind * types * unit declaration_hook Ephemeron.key
 
 (** {6 ... } *)
 (** [get_current_proof_name ()] return the name of the current focused
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 08eaa30f50..78f4923059 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -70,7 +70,7 @@ type pstate = {
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
   compute_guard : lemma_possible_guards;
-  hook : unit Tacexpr.declaration_hook;
+  hook : unit Tacexpr.declaration_hook Ephemeron.key;
   mode : proof_mode option;
 }
 
@@ -236,7 +236,7 @@ let start_proof id str goals ?(compute_guard=[]) hook =
     section_vars = None;
     strength = str;
     compute_guard = compute_guard;
-    hook = hook;
+    hook = Ephemeron.create hook;
     mode = None } in
   push initial_state pstates
 
@@ -262,7 +262,7 @@ let get_open_goals () =
 type closed_proof =
   Names.Id.t *
   (Entries.definition_entry list * lemma_possible_guards *
-    Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
+    Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key)
 
 let close_proof ~now fpl =
   let { pid;section_vars;compute_guard;strength;hook;proof } = cur_pstate () in
@@ -409,13 +409,12 @@ module V82 = struct
 end
 
 type state = pstate list
-let drop_hook_mode p = { p with hook = None; mode = None }
         
 let freeze ~marshallable =
   match marshallable with
   | `Yes ->
       Errors.anomaly (Pp.str"full marshalling of proof state not supported")
-  | `Shallow -> List.map drop_hook_mode !pstates
+  | `Shallow -> !pstates
   | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 9d7407010c..144b59f4d9 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -62,7 +62,7 @@ val start_proof : Names.Id.t ->
 type closed_proof =
   Names.Id.t *
   (Entries.definition_entry list * lemma_possible_guards *
-    Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
+    Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key)
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
@@ -143,7 +143,7 @@ end
 
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list *
-  Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
+  Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key)
 end
 
 type state
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index fafafd8534..3277393787 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1634,12 +1634,12 @@ let add_morphism_infer glob m n =
 	Flags.silently
 	  (fun () ->
 	    Lemmas.start_proof instance_id kind instance
-	      (Some (fun _ -> function
+	      (fun _ -> function
 		Globnames.ConstRef cst ->
 		  add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
 				   glob (ConstRef cst));
 		  declare_projection n instance_id (ConstRef cst)
-		| _ -> assert false));
+		| _ -> assert false);
 	    Pfedit.by (Tacinterp.interp tac)) ()
 
 let add_morphism glob binders m s n =
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 89cf116ca7..f9ce75bba7 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 fa5d405e21..c460e291c7 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 9efe4eefc8..1dbdcf78c0 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 5a936e6234..a25f96d469 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 8c74145687..3c4b88f46c 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 d63ef9ec12..eb40387211 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