The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq users,

I really like the primitive projections feature, because the let terms to 
which projections expand sometimes make proof contexts with large records 
hard to understand. Just it doesn't work as I expected.

In the below sample:

        Set Primitive Projections.

        Record Test := 
        {
          a : unit;
          b : bool;
          c : nat
        }.

        Print a.

I get

        a = fun t : Test => let (a, _, _) := t in a : Test -> unit

I expected that the let term would go away and be replaced by the new 
primitive projection term. Also if I try

        Definition test := Build_Test tt false 0.
        Definition testa := test.(a).
        Eval cbv delta beta in testa.

I get

     = let (a, _, _) := {| a := tt; b := false; c := 0 |} in a
     : unit

I used the 8.5beta1 windows version.

Best regards,

Michael