diff options
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 c264b19063..56f32196b6 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 ] |