coqhammer icon indicating copy to clipboard operation
coqhammer copied to clipboard

Published 20 hours ago • verified publisher icon lukaszcz

Adapt to Coq PR #6285

Open mattam82 opened this issue 3 years ago • 0 comments

For coq/coq#6285 (on top of #13952) This introduces an extension of Hint Extern, that is only available through typeclasses eauto in Coq. There is some continuation passing magic here so I'm not sure how to adapt sauto, but it can surely be done. Do not merge yet!

mattam82 avatar Mar 27 '21 11:03 mattam82