diff options
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index c6f09eb2d..7349a8273 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -76,6 +76,7 @@ let pf_apply f gls = f (pf_env gls) (project gls) let pf_eapply f gls x = on_sig gls (fun evm -> f (pf_env gls) evm x) let pf_reduce = pf_apply +let pf_e_reduce = pf_apply let pf_whd_betadeltaiota = pf_reduce whd_betadeltaiota let pf_hnf_constr = pf_reduce hnf_constr |