[Termtools] on the correctness of coq proofs

[Frederic Blanqui]

Dear all, here are new commands that could be useful to check that no 
lemma uses hidden axioms:

Message from Pierre Letouzey on coq-club on 29/11/08: "On the topic of 
axioms, a "Print eq_elim" after the above command
shows clearly that no axiom is used in the proof. This can also be
confirmed by the new command "Print Assumption eq_elim" whose aim is
to recursively retreive the axiom(s) a particular object is using.
Concerning standard tactics, apart obviously from "admit", I can see
none that might introduce axioms. And anyway, in case of doubt,
you can do a "Print Assumption" of your lemma. "