diff options
| author | Arnaud Spiwack | 2014-10-31 11:10:04 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | 674f353d32ec2dc957a2402e528290c4695e761b (patch) | |
| tree | 591a06899b0a45432774490c11f86ded831ca24d | |
| parent | bfa71dfcf722dfc0e1f1cd616945cc3e1da9d5ba (diff) | |
Info: the warning message of the defunct [info] tactic now points to the [Info] command.
| -rw-r--r-- | tactics/tacinterp.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 10f382a9e5..d589f0c180 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1168,8 +1168,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacArg a -> interp_tactic ist (TacArg a) | TacInfo tac -> msg_warning - (strbrk "The general \"info\" tactic is currently not working." ++ fnl () ++ - strbrk "Some specific verbose tactics may exist instead, such as info_trivial, info_auto, info_eauto."); + (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."); eval_tactic ist tac (* For extensions *) | TacAlias (loc,s,l) -> |