From c9917c210da30521673e843b626359f4a1051e74 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 22 Apr 2013 14:39:07 +0000 Subject: 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 --- proofs/redexpr.ml | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) (limited to 'proofs/redexpr.ml') 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) } -- cgit v1.2.3