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

4 files changed, 13 insertions, 13 deletions

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