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 1310fe7f9..57b8c5406 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 = + let input : bool * Tacexpr.glob_tactic_expr -> obj = declare_object { (default_object name) with cache_function = cache; |