search

coq-tactician / coq-tactician-api

An API for interfacing with Coq through Tactician by external agents
https://coq-tactician.github.io/api/introduction
MIT License
2 stars 1 forks source link

Tf search interface v9 #10

Closed LasseBlaauwbroek closed 2 years ago

LasseBlaauwbroek commented 2 years ago

I did some testing and everything seems to be working fine. So if you address the comments above, I think we are good to go!

LasseBlaauwbroek commented 2 years ago

Okay, I made some final tweaks. I think this is ready to be merged. @pestun the commit history of this PR is a bit messy. Do you mind if I squash it before the merge? Or do you want to keep the history?