The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 04/22/2017 11:35 PM, Kenneth Roe wrote:
> This solution does not quite work.  This does indeed apply vm_compute to the ?X 
> term.  However, this code will substitute the result or the existential variable.  
> The “reflexivity” tactic will then apply “simpl" to the original “3+4” term.  
> The “3+4” term needs to be evaluated exclusively by vm_compute and nothing else.

That's the point of the vm_cast, the reflexivity will be checked by 
vm_compute.

--
Laurent