diff options
| author | Pierre-Marie Pédrot | 2020-04-02 14:27:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-02 14:27:57 +0200 |
| commit | 1806d3f6d43020c3219186416b4c63e80af2f11c (patch) | |
| tree | 5afee0b9351121361c325fe7509557220c097d6f /plugins | |
| parent | 971c8e12078980417c5865948b742dee38bd8593 (diff) | |
| parent | f7a5f8a46bbb39f7694990603be875f2ca466e7d (diff) | |
Merge PR #12002: Cleanup tactic_option a bit
Reviewed-by: ppedrot
Diffstat (limited to 'plugins')
| -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 |