Adapt w.r.t. coq/coq#18996.

[ppedrot]

No description provided.

[ppedrot]

@gares this seems to be failing but I do not understand why. I get

Error: Destructing let on this type expects 2 variables.

in some elpi test but I don't see how this fix and the corresponding PR on master can change the current behaviour. Are you by any chance sending weirdly ill-formed case nodes to the pretyper before going through the kernel and relying on doing this failing early somewhere specifically?

[ppedrot]

Indeed, there is some trickery involved in detyping. I ended up emulating the old behaviour through an explicit registering in the upstream PR. @gares tell me if you're fine with the now explicit hack.

[gares]

Indeed, there is some trickery involved in detyping. I ended up emulating the old behaviour through an explicit registering in the upstream PR. @gares tell me if you're fine with the now explicit hack.

I missed this PR and I think it is a horrible hack. But I guess it is too late.