diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 5b81da74a6..47a16a3bc0 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -54,10 +54,7 @@ val get_debug : unit -> debug_info (** Adds an interpretation function for extra generic arguments *) -(* spiwack: the [Term.constr] argument is the conclusion of the goal, - for "casted open constr" *) -val interp_genarg : interp_sign -> Environ.env -> Evd.evar_map -> Term.constr -> Goal.goal -> - glob_generic_argument -> Evd.evar_map * Value.t +val interp_genarg : interp_sign -> glob_generic_argument -> Value.t Ftactic.t (** Interprets any expression *) val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tactic) -> unit Proofview.tactic |