search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
211 stars 31 forks source link

[coq] Use findlib name in add_known_plugin #135

Closed ejgallego closed 2 years ago

ejgallego commented 2 years ago

After some stronger invariant upstream, the name here has to match the name used in Declare ML Module and DECLARE PLUGIN

Should be backwards compatible.

ejgallego commented 2 years ago

@lukaszcz CI is not working (not due to this PR) , but I've checked it works, you can merge now if you want.