diff options
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 48c4f8d48..10f6be1d5 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -11,12 +11,8 @@ open Term open Context open Environ open Evd -open Reduction open Proof_type -open Refiner open Redexpr -open Tacexpr -open Glob_term open Pattern open Locus open Misctypes @@ -134,8 +130,6 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig - open Proofview - val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a val pf_global : identifier -> Proofview.Goal.t -> constr val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a |