@@ -1487,9 +1487,12 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
14871487 prettySe p bnd (PPi (Constraint _ _) n _ ty sc) =
14881488 bracket p startPrec $
14891489 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1490+ prettySe p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =
1491+ lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1492+ rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
14901493 prettySe p bnd (PPi (TacImp _ _ s) n _ ty sc) =
14911494 bracket p startPrec $
1492− lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1495+ lbrace <> kwd "default" <+> prettySe (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
14931496 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
14941497 -- This case preserves the behavior of the former constructor PEq.
14951498 -- It should be removed if feasible when the pretty-printing of infix
@@ -1621,9 +1624,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
16211624 prettySe p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
16221625 -- XXX: add pretty for tactics
16231626 prettySe p bnd (PProof ts) =
1624− text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1627+ kwd "proof" <+> lbrace <> text "..." <> rbrace
16251628 prettySe p bnd (PTactics ts) =
1626− text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1629+ kwd "tactics" <+> lbrace <> text "..." <> rbrace
16271630 prettySe p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
16281631 prettySe p bnd (PReturn f) = kwd "return"
16291632 prettySe p bnd PImpossible = kwd "impossible"