diff options
author | 2017-06-12 11:08:12 +0200 | |
---|---|---|
committer | 2017-06-12 11:08:12 +0200 | |
commit | 2253d2eb4f892f932332358be8537fdb5552ef87 (patch) | |
tree | 78825c9f5c9db43fc1e1b03ca26ba73cbdd98cfd /interp/constrextern.mli | |
parent | faa064c746e20a12b3c8f792f69537b18e387be6 (diff) |
Remove Show Implicit Arguments command.
The command has been broken for 15 years. It is basically dead code.
Its former behavior can be mimicked with Set Printing Implicit. Show.
Diffstat (limited to 'interp/constrextern.mli')
0 files changed, 0 insertions, 0 deletions