diff options
Diffstat (limited to 'parsing/ppvernac.ml')
| -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 c4ffbfd152..49c76c96ce 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -471,7 +471,6 @@ let rec pr_vernac = function | VernacCheckGuard -> str"Guarded" (* Resetting *) - | VernacRemoveName id -> str"Remove" ++ spc() ++ pr_lident id | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id | VernacResetInitial -> str"Reset Initial" | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i |