diff options
| author | Théo Zimmermann | 2016-10-19 18:30:44 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2016-10-25 16:06:13 +0200 |
| commit | d2e713c3913c995ba3796863f778556e00cc5051 (patch) | |
| tree | 110d408563b1b65438599f33ba1926e53bf88053 /kernel/cbytecodes.mli | |
| parent | 67b49d4d5afdd67bb0a81e3fdf6876387d28a36e (diff) | |
Remove warning now that info_auto is fixed.
Removes a warning dating from 8.5 signaling that info_auto
and info_trivial are broken and advising to use Info 1 auto
instead. Now, these tactics are fixed and thus they can be
used again. They do not do exactly the same thing as
Info 1 auto and may be more useful for the learner.
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions