diff options
Diffstat (limited to 'tactics/tactic_option.ml')
| -rw-r--r-- | tactics/tactic_option.ml | 25 |
1 files changed, 11 insertions, 14 deletions
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml index 561485833..7a13890b5 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 |