diff options
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e0dd3380f9..5eeeaada2d 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -887,10 +887,9 @@ open Pputils spc() ++ pr_class_rawexpr c2) ) - | VernacInstance (abst, sup, (instid, bk, cl), props, info) -> + | VernacInstance (sup, (instid, bk, cl), props, info) -> return ( hov 1 ( - (if abst then keyword "Declare" ++ spc () else mt ()) ++ keyword "Instance" ++ (match instid with | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc () @@ -906,13 +905,23 @@ open Pputils | None -> mt())) ) + | VernacDeclareInstance (sup, (instid, bk, cl), info) -> + return ( + hov 1 ( + keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++ + pr_and_type_binders_arg sup ++ + str":" ++ spc () ++ + (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ + pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info) + ) + | VernacContext l -> return ( hov 1 ( keyword "Context" ++ pr_and_type_binders_arg l) ) - | VernacDeclareInstances insts -> + | VernacExistingInstance insts -> let pr_inst (id, info) = pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info in @@ -922,7 +931,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) ) |