The Coq mailing list

[Bruno Barras <Bruno.Barras AT cl.cam.ac.uk>]

Hello,

As Jean-Christophe said, you can only suppress pretty-printing by overriding 
existing rules. However, the rule he proposed needs fine tuning:

> You  can  override the  current  pretty-printing  rules  by new  ones,
> following the current ones  defined in LogicSyntax.v. For instance, if
> you add:
> 
>     Syntax constr
>     level 6:
>       and [<< $t1 /\ $t2 >>] -> [ [<hov 0>"and" [1 0] $t1:L [1 0] $t2:E ] ].

Since you print [and] as a normal application, you should put the rule in the 
same level as application (ie 10, see src/syntax/PPCommand.v):

    Syntax constr level 10:
      and [<< $t1 /\ $t2 >>] -> [ [<hov 0>"and" (APPTAIL $t1 $t2):E ] ].

Another possibility which requires less knowledge is to change rule "and" so 
that it does not match any well-formed AST (declaring a rule with the same 
name as an existing one discards the old one).

    Syntax constr level 0:
      and [(DUMMY_PATTERN )] -> [ "This is a dummy rule" ].

Sincerely,

Bruno Barras.

-----------------------------------------
e-mail: 
bruno.barras AT cl.cam.ac.uk
www:    http://www.cl.cam.ac.uk/~bb236/
tel:    +44 (1223) 334688
-----------------------------------------