aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-24 14:35:25 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-25 17:42:55 +0200
commitbf4112094feb1a705d8bdaea3fb0febc4ef3ff59 (patch)
tree49bf826bd68429694abb86df757d54147fb80554 /tactics/tactics.ml
parent0897d0f642c19419c513f9609782436bebf28f5b (diff)
[general] Remove Econstr dependency from `intf`
To this extent we factor out the relevant bits to a new file, ltac_pretype.
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)