From 6bd193ff409b01948751525ce0f905916d7a64bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Nov 2016 14:38:35 +0100
Subject: Nativenorm API using EConstr.

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

(limited to 'proofs')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 348cd1bcbb..62fe2c17ca 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -37,9 +37,8 @@ let cbv_native env sigma c =
     (warn_native_compute_disabled ();
      cbv_vm env sigma c)
   else
-    let c = EConstr.Unsafe.to_constr c in
-    let ctyp = Retyping.get_type_of env sigma c in
-    Nativenorm.native_norm env sigma c ctyp
+    let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in
+    Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp)
 
 let whd_cbn flags env sigma t =
   let (state,_) =
-- 
cgit v1.2.3