diff options
| author | Gaëtan Gilbert | 2020-04-02 12:13:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-02 12:13:57 +0200 |
| commit | f7a5f8a46bbb39f7694990603be875f2ca466e7d (patch) | |
| tree | 475f8c3bdc928ff0a6f44133616df04d7376d1ab /plugins/ltac | |
| parent | d03529ab8fec0cad5705b5f775e43ef26c0dedcb (diff) | |
Cleanup tactic_option a bit
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/tactic_option.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml index c72a527537..4f00f17892 100644 --- a/plugins/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml @@ -13,15 +13,11 @@ open Pp let declare_tactic_option ?(default=Tacexpr.TacId []) name = 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 : Tacexpr.glob_tactic_expr ref = - Summary.ref !default_tactic_expr ~name:(name^"-default-tactic") + Summary.ref default ~name:(name^"-default-tactic") in let set_default_tactic local t = locality := local; - default_tactic_expr := t; default_tactic := t in let cache (_, (local, tac)) = set_default_tactic local tac in @@ -42,12 +38,11 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name = subst_function = subst} in let put local tac = - set_default_tactic local tac; Lib.add_anonymous_leaf (input (local, tac)) in let get () = !locality, Tacinterp.eval_tactic !default_tactic in let print () = - Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++ + Pptactic.pr_glob_tactic (Global.env ()) !default_tactic ++ (if !locality then str" (locally defined)" else str" (globally defined)") in put, get, print |