@@ -1484,9 +1484,12 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1484 prettySe p bnd (PPi (Constraint _ _) n _ ty sc) =
1484 prettySe p bnd (PPi (Constraint _ _) n _ ty sc) =
1485 bracket p startPrec $
1485 bracket p startPrec $
1486 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1486 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
1487 prettySe p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1490 prettySe p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1488 bracket p startPrec $
1491 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 <>
1490 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1493 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1491 -- This case preserves the behavior of the former constructor PEq.
1494 -- This case preserves the behavior of the former constructor PEq.
1492 -- It should be removed if feasible when the pretty-printing of infix
1495 -- It should be removed if feasible when the pretty-printing of infix
@@ -1618,9 +1621,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1618 prettySe p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1621 prettySe p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1619 -- XXX: add pretty for tactics
1622 -- XXX: add pretty for tactics
1620 prettySe p bnd (PProof ts) =
1623 prettySe p bnd (PProof ts) =
1621− text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1624+ kwd "proof" <+> lbrace <> text "..." <> rbrace
1622 prettySe p bnd (PTactics ts) =
1625 prettySe p bnd (PTactics ts) =
1623− text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1626+ kwd "tactics" <+> lbrace <> text "..." <> rbrace
1624 prettySe p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1627 prettySe p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1625 prettySe p bnd (PReturn f) = kwd "return"
1628 prettySe p bnd (PReturn f) = kwd "return"
1626 prettySe p bnd PImpossible = kwd "impossible"
1629 prettySe p bnd PImpossible = kwd "impossible"