Adapt to Coq PR #17987 which adds sigma to the API of search functions

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

Other

211 stars 31 forks source link

Closed herbelin closed 12 months ago

herbelin commented 1 year ago

The Coq PR is to fix #17963: sigma has to be passed to search functions.

It has to be merged synchronously with coq/coq#17987.

ppedrot commented 1 year ago

Please merge now.