diff options
| author | Théo Zimmermann | 2017-06-12 11:08:12 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-06-12 11:08:12 +0200 |
| commit | 2253d2eb4f892f932332358be8537fdb5552ef87 (patch) | |
| tree | 78825c9f5c9db43fc1e1b03ca26ba73cbdd98cfd /intf | |
| 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 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index ab440c6b71..c928e0bbbf 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -96,7 +96,6 @@ type locatable = type showable = | ShowGoal of goal_reference - | ShowGoalImplicitly of int option | ShowProof | ShowNode | ShowScript |