vm_compute produces an anomoly on meta-variables

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#2885
From: @gmalecha
Reported version: 8.4
CC: @herbelin, @maximedenes, nuno.gaspar@inria.fr, @ppedrot

Duplicates: BZ#5659

[coqbot]

Comment author: @gmalecha

When a term includes meta-variables, vm_compute produces an uncatchable anomoly. This makes it unusable when it is unknown whether an existential occurs. Is it possible to do any of the following:

1. Make vm_compute treat meta variables as regular context variables
2. Make vm_compute fail (with a regular ltac fail) when it encounters this problem
3. Write a tactical that catches anomolies and converts them into tactic failures.

I'm not sure which one is best to do.

[coqbot]

Comment author: @letouzey

*** Bug BZ#3169 has been marked as a duplicate of this bug. ***

[coqbot]

Comment author: @herbelin

Anomaly has now been changed to an error, but the wish for having vm_compute supporting evars is still there...

[coqbot]

Comment author: @maximedenes

I added experimental support for evars for the native compiler (native_compute) in the trunk. Testing and feedback welcome. Much of this could be reused for the VM.

[coqbot]

Comment author: @ppedrot

*** This bug has been marked as a duplicate of bug BZ#5659 ***