How does one print proof terms as de bruijn indices instead of random named variables in Coq?

[brando90]

I wanted to print/see my proof terms as de bruijn indices. How do I do this?

I know Show Proof. shows me the proof term.

Thanks!

---

• cross: How does one print proof terms as de bruijn indices instead of random named variables in Coq? - Stack Overflow
• metacoq gitissue: How does one print proof terms as de bruijn indices instead of random named variables in Coq? · Issue #808 · MetaCoq/metacoq · GitHub

[herbelin]

I don’t see a way (internally to Coq) to print binders of Coq terms with de Bruijn indices. You can probably do it however via MetaCoq.

By curiosity, what is the intended application?