lukaszcz / coqhammer

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

Don't use Mltop.add_known_plugin #153

Closed SkySkimmer closed 1 year ago

SkySkimmer commented 1 year ago

It will probably be removed eg in https://github.com/coq/coq/pull/17069

This is used only to automatically print the version when loading the plugin, there is already the Hammer_version command so IMO no point writing a replacement.

SkySkimmer commented 1 year ago

Please merge