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

7 files changed, 14 insertions, 14 deletions

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