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

1 files changed, 5 insertions, 11 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 828da8688..80d0ead96 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -20,7 +20,6 @@ open Tacred
 open Closure
 open RedFlags
 open Libobject
-open Summary
 open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
@@ -106,10 +105,10 @@ let inStrategy : strategy_obj -> obj =
 let set_strategy local str =
   Lib.add_anonymous_leaf (inStrategy (local,str))
 
-let _ = declare_summary "Transparent constants and variables"
-    { freeze_function = Conv_oracle.freeze;
-      unfreeze_function = Conv_oracle.unfreeze;
-      init_function = Conv_oracle.init }
+let _ = Summary.declare_summary "Transparent constants and variables"
+  { Summary.freeze_function = Conv_oracle.freeze;
+    Summary.unfreeze_function = Conv_oracle.unfreeze;
+    Summary.init_function = Summary.nop }
 
 
 (* Generic reduction: reduction functions used in reduction tactics *)
@@ -148,7 +147,7 @@ let reduction_tab = ref String.Map.empty
 
 (* table of custom reduction expressions, synchronized,
    filled by command Declare Reduction *)
-let red_expr_tab = ref String.Map.empty
+let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
 
 let declare_reduction s f =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
@@ -253,8 +252,3 @@ let inReduction : bool * string * red_expr -> obj =
 
 let declare_red_expr locality s expr =
     Lib.add_anonymous_leaf (inReduction (locality,s,expr))
-
-let _ = declare_summary "Declare Reduction"
-  { freeze_function = (fun () -> !red_expr_tab);
-    unfreeze_function = ((:=) red_expr_tab);
-    init_function = (fun () -> red_expr_tab := String.Map.empty) }