diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 7c731e2b9..5fa9c220d 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -27,7 +27,7 @@ type value = | VVoid | VInteger of int | VIntroPattern of intro_pattern_expr - | VConstr of constr + | VConstr of Pattern.constr_under_binders | VConstr_context of constr | VList of value list | VRec of (identifier*value) list ref * glob_tactic_expr @@ -39,8 +39,8 @@ and interp_sign = debug : debug_info; trace : ltac_trace } -val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env -> - Pretyping.var_map * Pretyping.unbound_ltac_var_map +val extract_ltac_constr_values : interp_sign -> Environ.env -> + Pretyping.ltac_var_map (** Transforms an id into a constr if possible *) val constr_of_id : Environ.env -> identifier -> constr |