diff options
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3b497faab5..e4558481bc 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1187,7 +1187,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with msg_warning (strbrk "The general \"info\" tactic is currently not working." ++ spc()++ strbrk "There is an \"Info\" command to replace it." ++fnl () ++ - strbrk "Some specific verbose tactics may also exist, such as info_trivial, info_auto, info_eauto."); + strbrk "Some specific verbose tactics may also exist, such as info_eauto."); eval_tactic ist tac (* For extensions *) | TacAlias (loc,s,l) -> |