diff options
| author | glondu | 2009-10-28 16:48:36 +0000 |
|---|---|---|
| committer | glondu | 2009-10-28 16:48:36 +0000 |
| commit | c14986c2fa8c8563f7da68d98b7c0b7f6ea2c9e7 (patch) | |
| tree | fc293a0e97ae8619ca629bccc14a48d62c02a925 /proofs | |
| parent | 7c151ae076fe5ebba9a2ea507f8f4a235feab9c7 (diff) | |
Remove old compatibility stuff (Tacred.nf)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacmach.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |