diff options
| -rw-r--r-- | printing/miscprint.ml | 4 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/printing/miscprint.ml b/printing/miscprint.ml index 7b2c5695fd..1ab6cc8b90 100644 --- a/printing/miscprint.ml +++ b/printing/miscprint.ml @@ -36,9 +36,9 @@ and pr_or_and_intro_pattern prc = function | IntroAndPattern pl -> str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")" | IntroOrPattern pll -> - str "[" ++ + str "[ " ++ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) - ++ str "]" + ++ str " ]" (** Printing of [move_location] *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4299f0f522..fb9dca255c 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1237,13 +1237,13 @@ module Make with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in try let rl = Egramml.get_extend_vernac_rule s in - let rec aux rl cl = + let rec aux sep rl cl = match rl, cl with - | Egramml.GramNonTerminal (_,_,e) :: rl, (GenArg (wit,x)) :: cl -> pr_based_on_grammar (GenArg (wit,x),EntryName e) :: aux rl cl - | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl + | Egramml.GramNonTerminal (_,_,e) :: rl, (GenArg (wit,x)) :: cl -> pr_based_on_grammar (GenArg (wit,x),EntryName e) :: aux sep rl cl + | Egramml.GramTerminal s :: rl, cl -> sep() ++ str s :: aux spc rl cl | [], [] -> [] | _ -> assert false in - hov 1 (pr_sequence (fun x -> x) (aux rl cl)) + hov 1 (pr_sequence (fun x -> x) (aux mt rl cl)) with Not_found -> hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_based_on_structure cl ++ str ")") |