diff options
| author | Pierre-Marie Pédrot | 2018-12-17 18:10:03 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-17 18:10:03 +0100 |
| commit | dff69611da6ac1ea0e61228ede3cc8e320fcd914 (patch) | |
| tree | 1486cac06f945a758eae56bdb7e7d4c8be5a7a14 /proofs/tacmach.ml | |
| parent | 28c7600cdc56ce7dfdabe058db57883a73653298 (diff) | |
| parent | 1d0e7063fe10fbf27a1b0a8296c69ed6b661d70e (diff) | |
Merge PR #9153: [api] Move reduction modules to `tactics`
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a5f691babb..df90354717 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -15,7 +15,6 @@ open Environ open Reductionops open Evd open Typing -open Redexpr open Tacred open Logic open Context.Named.Declaration @@ -71,11 +70,6 @@ let pf_global gls id = let sigma = project gls in Evd.fresh_global env sigma (Constrintern.construct_reference (pf_hyps gls) id) -let pf_reduction_of_red_expr gls re c = - let (redfun, _) = reduction_of_red_expr (pf_env gls) re in - let sigma = project gls in - redfun (pf_env gls) sigma 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) |