The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 29 Jun 2011 20:19:46 +0200,
Chris Dams 
<chris.dams.nl AT gmail.com>
 a écrit :

> Dear all,
> 
> After upgrading from 8.2pl2 to 8.3pl3, I noticed that records are no
> longer printed as (constructor_name arg1 ... argn) but instead as {|
> name1 := value1; ...; namen := valuen |}. I find this notation
> absolutely terrible because it makes the instances of records much
> longer. hypotheses that used to fit on one line now take FIVE. Please
> tell me how to switch it off.
> 
> All the best,
> Chris

It is not really a solution, but if you do not use the dot notation,
and you can freely reedit your code, use "Inductive" instead of record,
and that will do the trick.

Note also, that it is only for printing, so in the code you write, the
old notation stays available for writing; and for printing, may can you
use "aliases", that is for instance, replacing

s: T
H: P {| x := 0; y := 17|}
H0: Q {| x := 0; y := 17|} s
R: Z (f T) {| x := 0; y := 17 |}

with

s: T
pt := {| x := 0; y := 17|} 
H: P pt
H0: Q pt s
R: Z (f T) pt

or

s: T
pt: Point
Hptx: pt.(x) = 0
Hpty: pt.(y) = 17
H: P pt
H0: Q pt s
R: Z (f T) pt

for that there is the set tactic.

I am partly responsible for the introduction of this notation for the
records, and I know no way to deactivate it (maybe deactive notation
display could work, but I guess you don't want to do it).