diff options
| author | Hugo Herbelin | 2016-04-27 22:13:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:02 +0200 |
| commit | 1093c5e758f796b9dce3d870cb05f2c8a89bef43 (patch) | |
| tree | a5fc1da04f6160f45b7f1c1e80458ab2b5ea5abb /printing/miscprint.ml | |
| parent | f104dffa7661999bbbf405c2b0bb654758678bc6 (diff) | |
Revert "Fixing extra space in front of terminal in printing vernac."
This reverts commit 834885cb8cbc4d6924a63b898c7a5a32cfd0211c.
Diffstat (limited to 'printing/miscprint.ml')
| -rw-r--r-- | printing/miscprint.ml | 4 |
1 files changed, 2 insertions, 2 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] *) |