diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index f079d1dfb..254bb9fdd 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -73,13 +73,8 @@ val get_debug : unit -> debug_info (** Adds an interpretation function for extra generic arguments *) -type interp_genarg_type = - interp_sign -> goal sigma -> glob_generic_argument -> - Evd.evar_map * typed_generic_argument - -val add_interp_genarg : string -> interp_genarg_type -> unit - -val interp_genarg : interp_genarg_type +val interp_genarg : interp_sign -> goal sigma -> glob_generic_argument -> + Evd.evar_map * typed_generic_argument (** Interprets any expression *) val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> Evd.evar_map * value |