diff options
| author | Arnaud Spiwack | 2015-02-19 11:23:03 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-02-24 16:37:04 +0100 |
| commit | ebf4d8e58eeddaf5237447a9a0f21de48e72caa5 (patch) | |
| tree | 4ff0e577a13e8f459b513490812f031397640524 | |
| parent | 9ba579bb98ac8e8964a9baea376ce0c9a89f2615 (diff) | |
[info] tactical warning: do not suggest [info_auto] and [info_trivial].
Since they don't work anymore.
| -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) -> |