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 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 781af47892..2633cdd6b5 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -561,7 +561,6 @@ open Decl_kinds | GoalUid n -> spc () ++ str n in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n - | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n | ShowProof -> keyword "Show Proof" | ShowNode -> keyword "Show Node" | ShowScript -> keyword "Show Script" |