diff options
| author | Maxime Dénès | 2019-07-25 18:25:08 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-07-25 18:25:08 +0200 |
| commit | a352716c040280ed7c2cca84f0464b4081ec7727 (patch) | |
| tree | 054586778c132977319c04c3120d600f4ece4135 /plugins/syntax/r_syntax_plugin.mlpack | |
| parent | 3823ace92d92b2f5ee697ff156fe72d55217a921 (diff) | |
Remove deprecated `Backtrack` command
It has been deprecated since 8.4. The documentation was incorrect since
at least 8.5 (the last two arguments were ignored).
`Backtrack m n p` was a synonym for `BackTo m`
We also move `BackTo` handling to coqtop, since it is not meant to be
part of the document.
Diffstat (limited to 'plugins/syntax/r_syntax_plugin.mlpack')
0 files changed, 0 insertions, 0 deletions