diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index c51e753d46..f6d0807823 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -639,13 +639,14 @@ let map_constr_with_binders_left_to_right sigma g f l c = let al' = List.map_left (f l) al in if List.for_all2 (==) al' al then c else mkEvar (e, al') - | Case (ci,p,b,bl) -> + | Case (ci,p,iv,b,bl) -> (* In v8 concrete syntax, predicate is after the term to match! *) let b' = f l b in + let iv' = map_invert (f l) iv in let p' = f l p in let bl' = Array.map_left (f l) bl in - if b' == b && p' == p && bl' == bl then c - else mkCase (ci, p', b', bl') + if b' == b && p' == p && iv' == iv && bl' == bl then c + else mkCase (ci, p', iv', b', bl') | Fix (ln,(lna,tl,bl as fx)) -> let l' = fold_rec_types g fx l in let (tl', bl') = map_left2 (f l) tl (f l') bl in @@ -709,18 +710,20 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = | Evar (e,al) -> let al' = List.map (f l) al in if List.for_all2 (==) al al' then cstr else mkEvar (e, al') - | Case (ci,p,c,bl) when userview -> + | Case (ci,p,iv,c,bl) when userview -> let p' = map_return_predicate_with_full_binders sigma g f l ci p in + let iv' = map_invert (f l) iv in let c' = f l c in let bl' = map_branches_with_full_binders sigma g f l ci bl in - if p==p' && c==c' && bl'==bl then cstr else - mkCase (ci, p', c', bl') - | Case (ci,p,c,bl) -> + if p==p' && iv'==iv && c==c' && bl'==bl then cstr else + mkCase (ci, p', iv', c', bl') + | Case (ci,p,iv,c,bl) -> let p' = f l p in + let iv' = map_invert (f l) iv in let c' = f l c in let bl' = Array.map (f l) bl in - if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else - mkCase (ci, p', c', bl') + if p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else + mkCase (ci, p', iv', c', bl') | Fix (ln,(lna,tl,bl as fx)) -> let tl' = Array.map (f l) tl in let l' = fold_rec_types g fx l in |