From d528fdaf12b74419c47698cca7c6f1ec762245a3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:48:36 +0100 Subject: Retyping API using EConstr. --- proofs/redexpr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 62fe2c17c..19e72e697 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -24,7 +24,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = - let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + let ctyp = Retyping.get_type_of env sigma c in Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) let warn_native_compute_disabled = @@ -37,7 +37,7 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) else - let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) let whd_cbn flags env sigma t = -- cgit v1.2.3