diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-12 11:08:12 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 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 781af4789..2633cdd6b 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" |