From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 17:15:15 +0100 Subject: Removing compatibility layers in Retyping --- 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 a830e25d9..8878051c8 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -25,7 +25,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 c in - Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) + Vnorm.cbv_vm env sigma c ctyp let warn_native_compute_disabled = CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" @@ -38,7 +38,7 @@ let cbv_native env sigma c = cbv_vm env sigma c) else let ctyp = Retyping.get_type_of env sigma c in - Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) + Nativenorm.native_norm env sigma c ctyp let whd_cbn flags env sigma t = let (state,_) = -- cgit v1.2.3