diff options
| -rw-r--r-- | parsing/ppvernac.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index b181247ab4..8e7af67b0c 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -414,7 +414,6 @@ let rec pr_vernac = function | ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l in pr_showable s | VernacCheckGuard -> str"Guarded" - | VernacDebug b -> pr_topcmd b (* Resetting *) | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id |