diff options
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 2faf18355..695e8ab6e 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -75,6 +75,8 @@ let pf_reduction_of_red_expr gls re c = (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c 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_whd_betadeltaiota = pf_reduce whd_betadeltaiota |