diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-09 17:10:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-09 18:26:00 +0200 |
| commit | a2d3f5fc3167962f9bf549ba32f0105fff766422 (patch) | |
| tree | 1327eca1c50100bb5ef128f5a4dab0226986b368 /ltac | |
| parent | a2664de27eabbba7fc357305679112aef99e1f74 (diff) | |
Removing extra spaces in printing arguments of VERNAC EXTEND.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_ltac.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index c264b1906..56f32196b 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -354,7 +354,8 @@ VERNAC ARGUMENT EXTEND ltac_info PRINTED BY pr_ltac_info | [ "Info" natural(n) ] -> [ n ] END -let pr_ltac_use_default b = if b then str ".." else mt () +let pr_ltac_use_default b = + if b then (* Bug: a space is inserted before "..." *) str ".." else mt () VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default | [ "." ] -> [ false ] |