From c14986c2fa8c8563f7da68d98b7c0b7f6ea2c9e7 Mon Sep 17 00:00:00 2001
From: glondu
Date: Wed, 28 Oct 2009 16:48:36 +0000
Subject: Remove old compatibility stuff (Tacred.nf)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacmach.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 0faba52eae..754d98616f 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -98,7 +98,7 @@ let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
 let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_red_product               = pf_reduce red_product
-let pf_nf                        = pf_reduce nf
+let pf_nf                        = pf_reduce simpl
 let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
-- 
cgit v1.2.3