@@ -1484,9 +1484,12 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
14841484 prettySe p bnd (PPi (Constraint _ _) n _ ty sc) =
14851485 bracket p startPrec $
14861486 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1487+ prettySe p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =
1488+ lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1489+ rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
14871490 prettySe p bnd (PPi (TacImp _ _ s) n _ ty sc) =
14881491 bracket p startPrec $
1489− lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1492+ lbrace <> kwd "default" <+> prettySe (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
14901493 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
14911494 -- This case preserves the behavior of the former constructor PEq.
14921495 -- It should be removed if feasible when the pretty-printing of infix
@@ -1618,9 +1621,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
16181621 prettySe p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
16191622 -- XXX: add pretty for tactics
16201623 prettySe p bnd (PProof ts) =
1621− text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1624+ kwd "proof" <+> lbrace <> text "..." <> rbrace
16221625 prettySe p bnd (PTactics ts) =
1623− text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1626+ kwd "tactics" <+> lbrace <> text "..." <> rbrace
16241627 prettySe p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
16251628 prettySe p bnd (PReturn f) = kwd "return"
16261629 prettySe p bnd PImpossible = kwd "impossible"