aboutsummaryrefslogtreecommitdiff
path: root/pretyping/tacred.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r--pretyping/tacred.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 31cf52eace..a8cdfd8695 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -897,7 +897,7 @@ let contextually byhead (occs,c) f env sigma t =
else not (List.mem !pos locs) in
incr pos;
if ok then
- let subst' = List.map (on_snd (traverse envc)) subst in
+ let subst' = Id.Map.map (traverse envc) subst in
f subst' env sigma t
else if byhead then
(* find other occurrences of c in t; TODO: ensure left-to-right *)