Jason Gross

Let's see if https://github.com/rocq-community/run-coq-bug-minimizer/commit/8493589eae4d3ded130de711799a4e8be828bca8 helps, @coqbot ci minimize ci-paco

The relevant entry-point for the bedrock2 pipeline is https://github.com/mit-plv/fiat-crypto/blob/9bf41bc65f9cfb7263eda84fcfc878fe8da45ff7/src/Bedrock/Field/Stringification/Stringification.v#L200-L202 https://github.com/mit-plv/fiat-crypto/blob/9bf41bc65f9cfb7263eda84fcfc878fe8da45ff7/src/Bedrock/Field/Stringification/Stringification.v#L212-L220. As far as making `translate_func` avoid load/store when we only have one limb, I think @jadephilipoom or @andres-erbsen is better-placed...

I think you want to add a reification of `encode` (?) (the inverse of `eval`, I believe) a la https://github.com/mit-plv/fiat-crypto/blob/704fe3d9a1a25f28be568d703c352a70f57ac4a0/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v#L200-L210 or https://github.com/mit-plv/fiat-crypto/blob/704fe3d9a1a25f28be568d703c352a70f57ac4a0/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v#L224-L234 cf also https://github.com/mit-plv/fiat-crypto/blob/704fe3d9a1a25f28be568d703c352a70f57ac4a0/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v#L251-L256 Then we want versions of...

Yes, I would still like Coq to be pseudorelocatable in the way this PR tests

I see. I definitely want to locally control printing flags so I can print with printing records off. I am not sure about the difference between printing preterms vs printing...

@ppedrot Does your opinion also apply to https://github.com/rocq-prover/rocq/issues/21351#issue-3654155430 ?

What would the fix be, if we do want to fix it?

See also `expand_invisible` in https://github.com/rocq-prover/rocq/issues/3389

> It's not pretty and requires wrappers for the class itself and for all projections. Here is a version that does not require wrappers, but requires a `Hint Extern` for...

I think the more general thing @SkySkimmer is hinting at is that we can separate primitive projections from definitional eta; all records can be defined with primitive projections, but definitional...