Adapt to coq/coq#17633 (decompose_app returns array not list)

lukaszcz / coqhammer

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

Other

211 stars 31 forks source link

Closed SkySkimmer closed 1 year ago

SkySkimmer commented 1 year ago

This breaks async proofs and will probably break separation of parsing.

ppedrot commented 1 year ago

Please merge now.