diff options
| author | Emilio Jesus Gallego Arias | 2018-12-06 08:07:32 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-11 10:32:06 +0100 |
| commit | 913ccc7fb4a987ddd7c591d3c7d75579dc502a95 (patch) | |
| tree | 770f78f58393646c20e0ba007f3bb10ea4784dde /proofs/tacmach.ml | |
| parent | 97f5f37f782ffb9914fa8f67e745ba1effad20be (diff) | |
[api] Move reduction modules to `tactics`
These modules do actually belong there.
We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
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 64d7630d55..eed68b058b 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) |