From 2db085e62f7797cc999518eb58983ac059763e1f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Nov 2016 14:13:08 +0100
Subject: Vnorm API using EConstr.

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

(limited to 'proofs/redexpr.ml')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 40a8077a72..348cd1bcbb 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -24,11 +24,8 @@ open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
-  let c = EConstr.Unsafe.to_constr c in
-  let ctyp = Retyping.get_type_of env sigma c in
-  if Termops.occur_meta_or_existential sigma (EConstr.of_constr c) then
-    error "vm_compute does not support existential variables.";
-  Vnorm.cbv_vm env sigma c ctyp
+  let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in
+  Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp)
 
 let warn_native_compute_disabled =
   CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
-- 
cgit v1.2.3