MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
367 stars 79 forks source link

Fix typed erasure calls #1052

Closed mattam82 closed 6 months ago

mattam82 commented 6 months ago

We were asking to trim inductive masks whereas it made the check_expanded test always return false, so typed erasure was always the identity. We can now pass a dearging configuration to the typed pipeline.