@@ -1433,16 +1433,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
14331433 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
14341434 prettySe p bnd (PLam fc n ty sc) =
14351435 bracket p startPrec . group . align . hang 2 $
1436− text "\\" <> bindingOf n False <+> text "=>" <$>
1436+ text "\\" <> prettyBindingOf n False <+> text "=>" <$>
14371437 prettySe startPrec ((n, False):bnd) sc
14381438 prettySe p bnd (PLet fc n ty v sc) =
14391439 bracket p startPrec . group . align $
1440− kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1440+ kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
14411441 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
14421442 prettySe p bnd (PPi (Exp l s _) n ty sc)
14431443 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
14441444 bracket p startPrec . group $
1445− enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1445+ enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
14461446 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
14471447 | otherwise =
14481448 bracket p startPrec . group $
@@ -1455,7 +1455,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
14551455 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
14561456 | ppopt_impl ppo =
14571457 bracket p startPrec $
1458− lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1458+ lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
14591459 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
14601460 | otherwise = prettySe startPrec ((n, True):bnd) sc
14611461 where
@@ -1612,6 +1612,14 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
16121612
16131613 prettySe p bnd _ = text "missing pretty-printer for term"
16141614
1615+ prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1616+ prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1617+ where display (UN n) = T.unpack n
1618+ display (MN _ n) = T.unpack n
1619+ -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1620+ display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1621+ display n = show n
1622+
16151623 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
16161624 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
16171625 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm