Fixing extra space in front of terminal in printing vernac.

fix au revert [||]

2 files changed, 6 insertions, 6 deletions

diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 1ab6cc8b90..7b2c5695fd 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 fb9dca255c..4299f0f522 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 sep rl cl =
+      let rec aux rl cl =
         match rl, cl with
-        | 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
+        | 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
         | [], [] -> []
         | _ -> assert false in
-      hov 1 (pr_sequence (fun x -> x) (aux mt rl cl))
+      hov 1 (pr_sequence (fun x -> x) (aux rl cl))
     with Not_found ->
       hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_based_on_structure cl ++ str ")")