aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r--tactics/tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e8a78d72d..6ab643239 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -839,7 +839,7 @@ let e_change_in_hyp redfun (id,where) =
(convert_hyp c)
end
-type change_arg = Pattern.patvar_map -> evar_map -> evar_map * EConstr.constr
+type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr
let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c)