From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 19 Jan 2014 15:09:23 +0100
Subject: Imported Upstream version 8.4pl3dfsg

---
 proofs/redexpr.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'proofs')

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
 
 
-- 
cgit v1.2.3