The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

  Hi

> Firstly, I was wondering if it is possible to replace symbols in Coq with 
> other symbols. For example if I wanted to replace the \/ symbol.

  Yes, pretty-printing of "\/" is governed by the following rule
(in V7.0beta syntax)

Syntax constr
  level 7:
  or [ $t1 \/ $t2 ] -> [ [<hov 0> $t1:L [0 0]  "\\/" $t2:E ] ].

  Just overwrite the rule name above ("or") by your own rule, e.g. by

Syntax constr
  level 7:
  or [ (or $t1 $t2) ] -> [[<hov 0> $t1:L [0 0] " my_or_infix_syntax " $t2:E 
]].

Expressions such as :L and :E stand for associativity precedence and
brackets are for indentation purpose (please refer to the Coq
reference manual for further details). The names of the rules
governing pretty-printing can be found by typing the vernacular
command in src/syntax/PPConstr.v and in files *Syntax.v of the
library. (This is a bit hacky.)

  To enter a new parsing rule for "or", use Grammar.

  Hope it helps.
                                                  Hugo Herbelin