The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.fr>]

> How do I switch off pretty printing
> (in particular: and, or & ex) ?

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 ] ].

then A  /\ B will  be no longer printed  as A /\  B but as (and  A b),
which is what you want.

I'm not  a specialist of  PP in  Coq, and I  don't really know  is the
solution   above  is   fully  correct   regarding  the   insertion  of
parentheses. You can read the  reference manual for more details about
the way to define new pretty-printers:

      http://coq.inria.fr/doc/node.2.0.2.html

Best regards,
-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr