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 +
 pretyping/cbv.mli   | 2 +-
 pretyping/tacred.ml | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 87a03abbd9..3d17457679 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -19,7 +19,7 @@ open Esubst
 type cbv_infos
 
 val create_cbv_infos : RedFlags.reds -> env -> Evd.evar_map -> cbv_infos
-val cbv_norm         : cbv_infos -> constr -> constr
+val cbv_norm         : cbv_infos -> EConstr.constr -> constr
 
 (***********************************************************************
   i This is for cbv debug *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ac2a3bc490..c1e9573d27 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1136,7 +1136,7 @@ let fold_commands cl env sigma c =
 
 (* call by value reduction functions *)
 let cbv_norm_flags flags env sigma t =
-  cbv_norm (create_cbv_infos flags env sigma) (EConstr.Unsafe.to_constr t)
+  cbv_norm (create_cbv_infos flags env sigma) t
 
 let cbv_beta = cbv_norm_flags beta empty_env
 let cbv_betaiota = cbv_norm_flags betaiota empty_env
-- 
cgit v1.2.3