diff options
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 |