aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.mli
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-06-12 11:08:12 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-06-12 11:08:12 +0200
commit2253d2eb4f892f932332358be8537fdb5552ef87 (patch)
tree78825c9f5c9db43fc1e1b03ca26ba73cbdd98cfd /interp/constrextern.mli
parentfaa064c746e20a12b3c8f792f69537b18e387be6 (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