From 214a2ffd2cce3fa24908710af7db528a40345db6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 5 Nov 2016 18:24:20 +0100
Subject: Cbv API using EConstr.

---
 pretyping/cbv.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/cbv.ml')

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 84bf849e76..a42061f283 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -376,6 +376,7 @@ and cbv_norm_value info = function (* reduction under binders *)
 
 (* with profiling *)
 let cbv_norm infos constr =
+  let constr = EConstr.Unsafe.to_constr constr in
   with_stats (lazy (cbv_norm_term infos (subs_id 0) constr))
 
 type cbv_infos = cbv_value infos
-- 
cgit v1.2.3