code simplifications concerning Summary

 - Most of the time, the table registered via Summary.declare_summary
   is just a single reference. A new function Summary.ref now allows
   to both declare this ref and register it to summary in one shot.

 - Clarifications concerning the role of [init_function].
   For statically registered tables that don't need a special initializer,
   just do nothing there (see the new Summary.nop function).

 Beware: now that Summary exports a function named "ref", any code that
 do an "open Summary" will probably fail to compile.

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

5 files changed, 21 insertions, 64 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 38a616ddef..39e0c653c9 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -58,16 +58,7 @@ module HintDN = Term_dnet.Make(HintIdent)(HintOpt)
 
 (* Summary and Object declaration *)
 let rewtab =
-  ref (String.Map.empty : HintDN.t String.Map.t)
-
-let _ =
-  let init () = rewtab := String.Map.empty in
-  let freeze () = !rewtab in
-  let unfreeze fs = rewtab := fs in
-  Summary.declare_summary "autorewrite"
-    { Summary.freeze_function   = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function     = init }
+  Summary.ref (String.Map.empty : HintDN.t String.Map.t) ~name:"autorewrite"
 
 let raw_find_base bas = String.Map.find bas !rewtab
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 45a705f35a..8da15e8da7 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -276,20 +276,13 @@ let make_hints g st only_classes sign =
     (PathEmpty, []) sign
   in Hint_db.add_list hintlist (Hint_db.empty st true)
 
-let autogoal_hints_cache : (bool * Environ.named_context_val * hint_db) option ref = ref None
+let autogoal_hints_cache
+    : (bool * Environ.named_context_val * hint_db) option ref
+    = Summary.ref None ~name:"autogoal-hints-cache"
 let freeze () = !autogoal_hints_cache
 let unfreeze v = autogoal_hints_cache := v
-let init () = autogoal_hints_cache := None
 
-let _ = init ()
-
-let _ =
-  Summary.declare_summary "autogoal-hints-cache"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
-    
-let make_autogoal_hints = 
+let make_autogoal_hints =
   fun only_classes ?(st=full_transparent_state) g ->
     let sign = pf_filtered_hyps g in
       match freeze () with
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a8188d5820..0ec167873d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -406,7 +406,6 @@ END
 
 open Tactics
 open Glob_term
-open Summary
 open Libobject
 open Lib
 
@@ -415,8 +414,8 @@ open Lib
      x R y -> x == z -> z R y    (in the left table)
 *)
 
-let transitivity_right_table = ref []
-let transitivity_left_table = ref []
+let transitivity_right_table = Summary.ref [] ~name:"transitivity-steps-r"
+let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l"
 
 (* [step] tries to apply a rewriting lemma; then apply [tac] intended to
    complete to proof of the last hypothesis (assumed to state an equality) *)
@@ -448,24 +447,6 @@ let inTransitivity : bool * constr -> obj =
     subst_function = subst_transitivity_lemma;
     classify_function = (fun o -> Substitute o) }
 
-(* Synchronisation with reset *)
-
-let freeze () = !transitivity_left_table, !transitivity_right_table
-
-let unfreeze (l,r) =
-  transitivity_left_table := l;
-  transitivity_right_table := r
-
-let init () =
-  transitivity_left_table := [];
-  transitivity_right_table := []
-
-let _ =
-  declare_summary "transitivity-steps"
-    { freeze_function = freeze;
-      unfreeze_function = unfreeze;
-      init_function = init }
-
 (* Main entry points *)
 
 let add_transitivity_lemma left lem =
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index db2c19f006..d1abdd0af4 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -155,17 +155,12 @@ let lookup_tactic s =
 
 (* Summary and Object declaration *)
 
-let mactab = ref (Gmap.empty : (ltac_constant,glob_tactic_expr) Gmap.t)
+let mactab =
+  Summary.ref (Gmap.empty : (ltac_constant,glob_tactic_expr) Gmap.t)
+    ~name:"tactic-definition"
 
 let lookup_ltacref r = Gmap.find r !mactab
 
-let _ =
-  Summary.declare_summary "tactic-definition"
-    { Summary.freeze_function   = (fun () -> !mactab);
-      Summary.unfreeze_function = (fun fs -> mactab := fs);
-      Summary.init_function     = (fun () -> mactab := Gmap.empty); }
-
-
 
 (* We have identifier <| global_reference <| constr *)
 
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index 5614858335..7a13890b57 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -10,12 +10,17 @@ open Libobject
 open Pp
 
 let declare_tactic_option ?(default=Tacexpr.TacId []) name =
-  let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref default in
-  let default_tactic : Proof_type.tactic ref = ref (Tacinterp.eval_tactic !default_tactic_expr) in
-  let locality = ref false in
-  let set_default_tactic local t = 
+  let locality = Summary.ref false ~name:(name^"-locality") in
+  let default_tactic_expr : Tacexpr.glob_tactic_expr ref =
+    Summary.ref default ~name:(name^"-default-tacexpr")
+  in
+  let default_tactic : Proof_type.tactic ref =
+    ref (Tacinterp.eval_tactic !default_tactic_expr)
+  in
+  let set_default_tactic local t =
     locality := local;
-    default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t 
+    default_tactic_expr := t;
+    default_tactic := Tacinterp.eval_tactic t
   in
   let cache (_, (local, tac)) = set_default_tactic local tac in
   let load (_, (local, tac)) =
@@ -43,12 +48,4 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
     Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++
       (if !locality then str" (locally defined)" else str" (globally defined)")
   in
-  let freeze () = !locality, !default_tactic_expr in
-  let unfreeze (local, t) = set_default_tactic local t in
-  let init () = () in
-    Summary.declare_summary name
-      { Summary.freeze_function = freeze;
-        Summary.unfreeze_function = unfreeze;
-        Summary.init_function = init };
-    put, get, print
-      
+  put, get, print