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