I'm trying to get better parameter names in the types of projections https://github.com/coq/coq/issues/13727
I think all I have to do is to pick a binder name for the record that does not occur in the record declaration. How to get the set of bound names in a
constr? Should that be just a loop using
destProd? If I can do that then I figure that I can use
Namegen.next_ident_away to get a fresh enough name.
If there's a better way to do all of that I'm all ears.
Last updated: Oct 16 2021 at 07:02 UTC