diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 11 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 11 |
2 files changed, 13 insertions, 9 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 6e40e03f5b..fcc30d702f 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -219,7 +219,7 @@ module Make | ConstrContext ((_,id),c) -> hov 0 (keyword "context" ++ spc () ++ pr_id id ++ spc () ++ - str "[" ++ prlc c ++ str "]") + str "[ " ++ prlc c ++ str " ]") | ConstrTypeOf c -> hov 1 (keyword "type of" ++ spc() ++ prc c) | ConstrTerm c when test c -> @@ -630,7 +630,8 @@ module Make | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,()) in pr_in - (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs) + (prlist_with_sep (fun () -> str",") + (fun id -> spc () ++ pr_hyp_location pr_id id) l ++ pr_occs) let pr_orient b = if b then mt () else str "<- " @@ -675,9 +676,9 @@ module Make | Subterm (b,None,a) -> (** ppedrot: we don't make difference between [appcontext] and [context] anymore, and the interpretation is governed by a flag instead. *) - keyword "context" ++ str" [" ++ pr_pat a ++ str "]" + keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]" | Subterm (b,Some id,a) -> - keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]" + keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]" let pr_match_hyps pr_pat = function | Hyp (nal,mp) -> @@ -1216,7 +1217,7 @@ module Make | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> - str "ltac:(" ++ pr_tac (1,Any) (TacArg (Loc.ghost,a)) ++ str ")" + hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a)))) in pr_tac diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 3494ad006f..5d6d36d569 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -913,7 +913,7 @@ module Make | VernacContext l -> return ( hov 1 ( - keyword "Context" ++ spc () ++ pr_and_type_binders_arg l) + keyword "Context" ++ pr_and_type_binders_arg l) ) | VernacDeclareInstances insts -> @@ -1015,7 +1015,10 @@ module Make (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers - (match compat with None -> [] | Some v -> [SetCompatVersion v])) + (match compat with + | None -> [] + | Some Flags.Current -> [SetOnlyParsing] + | Some v -> [SetCompatVersion v])) ) | VernacDeclareImplicits (q,[]) -> return ( @@ -1057,7 +1060,7 @@ module Make in print_arguments nargs args ++ if not (List.is_empty more_implicits) then - str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits + prlist (fun l -> str"," ++ print_implicits l) more_implicits else (mt ()) ++ (if not (List.is_empty mods) then str" : " else str"") ++ prlist_with_sep (fun () -> str", " ++ spc()) (function @@ -1128,7 +1131,7 @@ module Make | VernacSetAppendOption (na,v) -> return ( hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++ - spc() ++ keyword "Append" ++ spc() ++ str v) + spc() ++ keyword "Append" ++ spc() ++ qs v) ) | VernacAddOption (na,l) -> return ( |