diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index a9fc8fa14..96c6da91f 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -152,9 +152,6 @@ val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr val hide_interp : raw_tactic_expr -> tactic option -> tactic -(** Declare the default tactic to fill implicit arguments *) -val declare_implicit_tactic : tactic -> unit - (** Declare the xml printer *) val declare_xml_printer : (out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit |