diff options
Diffstat (limited to 'tactics/tactic_option.ml')
-rw-r--r-- | tactics/tactic_option.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml index d0fa46c7a..1310fe7f9 100644 --- a/tactics/tactic_option.ml +++ b/tactics/tactic_option.ml @@ -25,7 +25,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name = let subst (s, (local, tac)) = (local, Tacinterp.subst_tactic s tac) in - let input, _output = + let input = declare_object { (default_object name) with cache_function = cache; |