The Coq mailing list

[Wojciech Moczydlowski <wm174746 AT zodiac.mimuw.edu.pl>]

  Hello,

here is the transcript of a short session with Coq. 
---------------------------------------------------------
Coq < Definition f : nat -> nat -> { x : nat & nat }.
1 subgoal

  ============================
   nat -> nat -> sigS (fun _ : nat => nat)

f < intros.
1 subgoal

  H : nat
  H0 : nat
  ============================
   sigS (fun _ : nat => nat)

f < exists H0.
1 subgoal

  H : nat
  H0 : nat
  ============================
   nat

f < exact O.
Proof completed.

f < Save.
intros.
exists H0.
exact 0.
f is defined

Coq < Eval compute in projS1 (f 20 20).
     = let (a, _) := f 20 20 in a
     : nat
-------------------------------------------
My question is - why does the last command give this answer, which 
doesn't seem to be reduced enough? I would expect it to evaluate to 20. 

Thanks,

Wojtek