Querying proof state in coq-serapi `Query (PrettyStrings, Lists) Goals`

[brando90]

I wanted to be able to get the entire current proof state (local context and goals) with all the individual terms separated, e.g. each term in a lists/arrays.

Pseduocode:

Recall usual Query cmd: (Query ((opt value) ...) kind) 

(Query (PrettyStrings, Lists) Goals)

Get back from Serapi something like:

(Response (LocalContext=[n: nat], Goals=[n + 0 = n], GlobalContext=[]) Completed) 

Ideally the terms can be in a format we want but I personally prefer normal Coq strings.

Bonus: as a bonus it would be nice to have a list of a few of the global context elements too.