Replace calls to "vm_compute in hyps" by plain calls to vm_compute.

[silene]

The terms are of type Internal.T env_sym, so invoking vm_compute in on them ends up strongly normalizing the function env_sym, which explodes. By using eval vm_compute instead, only the bodies get strongly normalized.

This is related to coq/coq#18917.

[SkySkimmer]

Is this different from vm_compute in (value of x)?

[palmskog]

@silene fine by me, do you advise this should be merged right away?

[silene]

@SkySkimmer No, it is the same. (That said, the location of the casts in the produced proof term might be slightly different. I never remember the precise rules for change, unfold, and vm_compute.)

@palmskog No hurry. It will only make things faster for users of aac_normalise, which I don't know if there are. So, it can wait until the next release.

[SkySkimmer]

Until https://github.com/coq/coq/pull/18796 there is no cast when using in hyp regardless of base tactic used.