aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/tactic_option.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index 7a13890b57..fdd5a9aaed 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -15,7 +15,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
Summary.ref default ~name:(name^"-default-tacexpr")
in
let default_tactic : Proof_type.tactic ref =
- ref (Tacinterp.eval_tactic !default_tactic_expr)
+ Summary.ref (Tacinterp.eval_tactic !default_tactic_expr) ~name:(name^"-default-tactic")
in
let set_default_tactic local t =
locality := local;