diff options
Diffstat (limited to 'proofs/tacmach.ml')
| -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 d41541251..bdcb4868b 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -87,7 +87,7 @@ let pf_e_reduce = pf_apply let pf_whd_all = pf_reduce whd_all let pf_hnf_constr = pf_reduce hnf_constr let pf_nf = pf_reduce simpl -let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) +let pf_nf_betaiota = pf_reduce nf_betaiota let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) let pf_unsafe_type_of = pf_reduce unsafe_type_of |