aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/miscops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/miscops.ml')
-rw-r--r--pretyping/miscops.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 10129306d..9ec031fbb 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -49,7 +49,8 @@ let map_occs f (occ,e) = (occ,f e)
let map_red_expr_gen f g h = function
| Fold l -> Fold (List.map f l)
| Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
- | Simpl occs_o -> Simpl (Option.map (map_occs (map_union g h)) occs_o)
+ | Simpl (flags,occs_o) ->
+ Simpl (map_flags g flags, Option.map (map_occs (map_union g h)) occs_o)
| Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
| Cbv flags -> Cbv (map_flags g flags)
| Lazy flags -> Lazy (map_flags g flags)