diff options
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 8be43c9495..3a3da8e2d8 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -922,7 +922,7 @@ open Pputils spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts) ) - | VernacDeclareClass id -> + | VernacExistingClass id -> return ( hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id) ) |