I would like to create a database of unfoldable constants and manipulate it programmatically. I wondered whether it would be possible to access an unfolding hint database from Ltac2, or if it is possible to implement my own hint database mechanism using Ltac2 references.
2 Likes