Dear Coq developers,
I want to get the information(constants and inductives) needed for current proof in coq while doing proof. For example, get the information while using copide. I think I need to extract the global environment of the proof.
I know I can use “Global.env ()” to get the global environment, but without printing it I am not sure whether “Global.env ()” is truly needed by me. Therefore I am trying to print the global environment.
I know I can use serapi’s command (Query () Env()) to get the global environment of the proof.
But it seems serapi can not be used while doing the proof in copide.
I have seen the “printer.ml” file in coq source, but I have not seen a function print the global environment.
I can use coq tactic “Print All“ to display the current state of the environment. But “Print All” is different from the (Query () Env()). It seems (Query () Env()) can just return the needed information(constants and inductives) of the current proof, while “Print All” can only display all the information(theorems, definitions, lemmas….) available in the current environment.
Therefore I have some questions.
1 Is “Global.env ()” the thing needed by me?
2 If it is not, what is the thing needed by me? Could I print it?
Best regards,
Zhang