Upgrade for Coq 8.11 - Githubissues

gmalecha / coq-ltac-iter

Access hint databases from tactics.

MIT License

12 stars 3 forks source link

Upgrade for Coq 8.11 #8

Closed Tuplanolla closed 4 years ago

Tuplanolla commented 4 years ago

I wanted to upgrade this plugin to work with Coq version 8.11. However, I have no idea what I am doing, so, while this attempt compiles and imports properly, it fails with syntax errors on ne_collection_list. I also applied some violence to tclIDTAC_MESSAGE, which loses an error message along the way; sorry about that.

It would nice if you could finish what I started here, because this plugin seems quite useful.

gmalecha commented 4 years ago

Thanks! @Tuplanolla

Tuplanolla commented 4 years ago

Note that this still fails with syntax errors on ne_collection_list.