The Coq mailing list

[Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>]

On 15.07.2014 14:34, Pierre Letouzey wrote:
> 
> 
> ----- Mail original -----
>>
>> This leads me to the second part of your report, which is far more severe:
>> something informative (in Coq's type "sum") is suddenly considered as
>> logical by the system (i.e. acceptable in sort "Prop"), and hence discarded
>> by the extraction, leading to this faulty "match __ with ...". This is
>> normally impossible in the good old theory of Coq, but this theory around
>> universes has been so much tweaked in the recent years (Hugo) and months
>> (Matthieu) that the very foundational principles of extraction need to be
>> re-asserted, and probably adapted, as shown by this bug. Once again, I'll
>> let you know when I know more.
>>
>> Best regards,
>> Pierre Letouzey
>>
> 
> Hi again
> 
> The "sum" instance being in "Prop" was actually a bug, now fixed in coq 
> trunk
> by Matthieu (commit 2b833c49). Since this commit, your development needs to 
> be
> slightly adapted accordingly :
>  - in Prefix.prefix_common you cannot inverse an "exists" to build
>    a "sum", now that this "sum" isn't in Prop anymore. 
>  - in Combi, a few "H" are now "X"
>  - in DeflateCoding, a few "sum" should rather be some "or" now.
> Here comes a temptative patch. With it, things compile and extract nicely
> (even if I've still the issue with Vector.t/VectorDef.t to investigate).
> 
> Best regards
> Pierre
> 

Thank you! It works!

Best regards
CSS