search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
42 stars 24 forks source link

Adapt w.r.t. coq/coq#16004 #66

Closed Alizter closed 2 years ago

samuelgruetter commented 2 years ago

This fails on our CI because in Coq 8.13, Hint Rewrite does not support #[global]. I'd personally solve this by simply dropping support for Coq <= 8.13, but before doing that, I feel I should ping @JasonGross, what do you think about that?

Alizter commented 2 years ago

I know @JasonGross keeps old versions around usually for the Debian packages.

JasonGross commented 2 years ago

dropping support for Coq <= 8.13

Can't we just fix this by adding -arg -w -arg -unsupported-attributes to _CoqProject

samuelgruetter commented 2 years ago

Can't we just fix this by adding -arg -w -arg -unsupported-attributes to _CoqProject

That would be fine with me!