The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Guillaume Brunerie wrote:
> But I do not understand why this is working. I had the impression that 
> Coq does not support dependent pattern matching. Perhaps there is a 
> limited dependent pattern matching support for simple types like 
> integers? 

My guess is you've formed this conclusion based on propaganda from the 
Agda community. ;)

> By the way, I’m working on homotopy type theory where fully general 
> dependent pattern matching is inconsistent (because it implies 
> Streicher’s axiom K for instance). Is it ok to use dependent pattern 
> matching on integers anyway?

Now I know that must be it! :)

There are many different feasible rules for dependent pattern matching.  
Coq's are based on explicit [match] annotations and tend to get the job 
done for almost all cases, even without relying on K.