The Coq mailing list

[Erik Ernst <eernst AT cs.au.dk>]

Hello again,

note that the typing dilemma that I just described can be avoided by not 
including P in the pattern match (so we would have 'match N1,N2 return..' 
rather than 'match N1,N2,P return', with corresponding changes in each 
branch), but this means that P will not have a type which reflects the extra 
knowledge about N1 and N2 that we gain by being in a specific branch of the 
match (so we always have 'P: R N1 N2' where otherwise we get 'P: R natO natO' 
in the first branch and so on), and that is quite important in the original 
context.

  best regards,

-- 
Erik Ernst - 
eernst AT cs.au.dk
Department of Computer Science, Aarhus University
IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark