summaryrefslogtreecommitdiff
path: root/proofs/redexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/redexpr.ml')
-rw-r--r--proofs/redexpr.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index d5750cfa..9d1d081e 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -22,8 +22,10 @@ open Libobject
open Summary
(* call by value normalisation function using the virtual machine *)
-let cbv_vm env _ c =
- let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
+let cbv_vm env sigma c =
+ let ctyp = Retyping.get_type_of env sigma c in
+ if Termops.occur_meta_or_existential c then
+ error "vm_compute does not support existential variables.";
Vnorm.cbv_vm env c ctyp