Emilio Jesús Gallego Arias

@Gopiandcode , not a lot of progress on this, as indeed current `Search.search` does a linear traverse of the objects in Coq's scope, so I was hoping we could have...

The `Init` call should also include the feedback initalization parameters, including the desired printing format.

cc #17

> I am interested in a Python way to use SerAPI. At what stage is this? I have thought a lot about ways to do it well, however not having...

> Sounds good! I'm happy to get together to help and chat about the interface/API/design etc. (if thats helpful/useful). That's great! > As a selfish comment, I am interesting to...

> steps like: `treat_equalities; assert_congs_perm; try split; finish.` are treated like a single compound tactic that affects multiple proof states (context+goal) in the proof tree. Ideally I'd like to control...

This took some time, but it is currently "solved" by https://github.com/ejgallego/pycoq However, due to toolchain issues, python support has not yet landed in the main branches, so we will keep...

Hey @brando90 ; oh, I totally missed that project when doing some search ; maybe I saw it back in March when I started PyCoq' :S would be helpful if...

> I am curious, why are RPCs not flexible? You are limited by the RPC interface, in this sense you have several limits: for example, depend on the chosen serialization...

> I am curious, why is it faster? I guess I am still struggling to form a model of how this is different from RPCs. Both have to eventually or...