diff options
Diffstat (limited to 'tactics/tactic_option.ml')
| -rw-r--r-- | tactics/tactic_option.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml index 10e79f733f..d0fa46c7a1 100644 --- a/tactics/tactic_option.ml +++ b/tactics/tactic_option.ml @@ -10,9 +10,9 @@ open Libobject open Proof_type open Pp -let declare_tactic_option name = - let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC in - let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId []) in +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 = locality := local; |