From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- pretyping/tacred.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/tacred.ml') diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 3fc01c86c..2b496f926 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1133,7 +1133,7 @@ let fold_commands cl env sigma c = (* call by value reduction functions *) let cbv_norm_flags flags env sigma t = - EConstr.of_constr (cbv_norm (create_cbv_infos flags env sigma) 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