diff options
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) |