Constr-as-datatype functions now use the user name for references.

[ppedrot]

This is a follow-up of #21863. Since it is clear that these functions are only used by plugins to manipulate terms as blobs, we should not try to be too clever by half, so we just ignore the aliasing quotient.

[SkySkimmer]

Plugins really want the quotienting. Possible solutions:

• access Global.env
• functorize the API module ConstrData (_:sig val env : env end) : sig ... end (works if used at constant delta resolver, nontrivial overlay work?)
• change to type t = env * constr and use one of the envs when comparing (but which side's env? I guess picking the side in which both constants appear when we encounter a constant? (if no side has both constants assert false)) probably easier overlay work
• don't change ConstrData but provide a canonize_constr : env -> contr -> constr function and have plugins use it before adding/looking up (costly?)

[SkySkimmer]

change to type t = env * constr and use one of the envs when comparing (but which side's env? I guess picking the side in which both constants appear when we encounter a constant? (if no side has both constants assert false)) probably easier overlay work

actually we can canonize each side using the respective env then compare the canonized kernames
maybe this solution is what we should do?

[ppedrot]

Yes, my plan to solve this is to canonize the term before storing it in the environment but then I need to understand what part of the code really relies on that.

[ppedrot]

The metacoq CI can be fixed via a one-liner, given the rest of the CI I'm not sure it's worth it to try to restore the previous behaviour for congruence / firstorder.

[ppedrot]

I normalized the terms in aac-tactics before storing them in the hashtable and it seems to have been enough for all tests to pass. In my opinion this PR is ready.

[SkySkimmer]

@coqbot merge now