The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 27 juin 09 à 19:53, Adam Koprowski a écrit :

> In short, this works: [...]
>   Thanks! I'll try to see whether I can make it work on my real  
> problem...
>
> For the generation of equalities for the toplevel dependent pattern- 
> matching,
> you should get them for free! The automatic inference of the return  
> predicate
> was not getting the dependency of the return type in [x], but this  
> can be fixed.
> As a result, you get to prove the [correct] tcc in each branch  
> instead of having
> to destruct the whole term again and get into these dependency  
> problems.
>   Indeed in my previous (simpler) version of this function, when [x]  
> was not dependently typed, that was the case: I got one tcc per  
> branch, with equality constraints and everything worked beautifully.
>   By 'this can be fixed' you mean the treatment of such cases by  
> Program? Or is there anything I can do to avoid providing the return  
> clause and benefiting from the Program's extra treatment of pattern  
> matching?

It is fixed in the trunk now, enjoy !

-- Matthieu