Matthieu Sozeau (Jul 05 2020 at 13:50): Matthieu Sozeau (Jul 05 2020 at 13:50):As was revealed during the Coq Workshop talk of Bohdan Liesnikov, the current param_original.v translation is buggy w.r.t universes and also fix-case, and requires some post-processing for their use case. @Cyril Cohen had a PR implementing fixes to it, we should integrate it.
Yannick Forster (Jul 05 2020 at 13:54):I think @Marcel Ullrich has a concrete example which fails, namely applying the translation to sigT
Cyril Cohen (Jul 05 2020 at 13:55):Matthieu Sozeau said:
As was revealed during the Coq Workshop talk of Bohdan Liesnikov, the current
param_original.vtranslation is buggy w.r.t universes and also fix-case, and requires some post-processing for their use case. Cyril Cohen had a PR implementing fixes to it, we should integrate it.
https://github.com/MetaCoq/metacoq/pull/94/files
Marcel Ullrich (Jul 05 2020 at 14:31):SigT seems to work, my mistake was at another point.
But certain types like roseTree have errors.
Inductive roseTree := tree (h:list roseTree).
Last updated: Apr 19 2024 at 16:01 UTC