diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index f6d0807823..e5231ef9cd 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -659,6 +659,12 @@ let map_constr_with_binders_left_to_right sigma g f l c = if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then c else mkCoFix (ln,(lna,tl',bl')) + | Array(u,t,def,ty) -> + let t' = Array.map_left (f l) t in + let def' = f l def in + let ty' = f l ty in + if def' == def && t' == t && ty' == ty then c + else mkArray(u,t',def',ty') let map_under_context_with_full_binders sigma g f l n d = let open EConstr in @@ -738,6 +744,11 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr else mkCoFix (ln,(lna,tl',bl')) + | Array(u,t,def,ty) -> + let t' = Array.Smart.map (f l) t in + let def' = f l def in + let ty' = f l ty in + if def==def' && t == t' && ty==ty' then cstr else mkArray (u,t', def',ty') let map_constr_with_full_binders sigma g f = map_constr_with_full_binders_gen false sigma g f |