EConstr iterators respect the binding structure of cases.

Fixes #3166.

1 files changed, 23 insertions, 13 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index d331ecc458..4dc584cfa8 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -651,15 +651,19 @@ let map_constr_with_binders_left_to_right env sigma g f l c =
       if List.for_all2 (==) al' al then c
       else mkEvar (e, al')
   | Case (ci,u,pms,p,iv,b,bl) ->
-      (* FIXME: skip annotations? *)
-      let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, b, bl) in
+      let (ci, _, pms, p0, _, b, bl0) = annotate_case env sigma (ci, u, pms, p, iv, b, bl) in
+      let f_ctx (nas, _ as r) (ctx, c) =
+        let c' = f (List.fold_right g ctx l) c in
+        if c' == c then r else (nas, c')
+      in
       (* In v8 concrete syntax, predicate is after the term to match! *)
       let b' = f l b in
+      let pms' = Array.map_left (f l) pms in
+      let p' = f_ctx p p0 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 && iv' == iv && bl' == bl then c
-      else mkCase (EConstr.contract_case env sigma (ci, p', iv', b', bl'))
+      let bl' = Array.map_left (fun (c, c0) -> f_ctx c c0) (Array.map2 (fun x y -> (x, y)) bl bl0) in
+        if b' == b && pms' == pms && p' == p && iv' == iv && bl' == bl then c
+        else mkCase (ci, u, pms', 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
@@ -713,13 +717,18 @@ let map_constr_with_full_binders env sigma g f l cstr =
       let al' = List.map (f l) al in
       if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
   | Case (ci, u, pms, p, iv, c, bl) ->
-      let (ci, p, iv, c, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in
-      let p' = f l p in
+      let (ci, _, pms, p0, _, c, bl0) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+      let f_ctx (nas, _ as r) (ctx, c) =
+        let c' = f (List.fold_right g ctx l) c in
+        if c' == c then r else (nas, c')
+      in
+      let pms' = Array.Smart.map (f l) pms in
+      let p' = f_ctx p p0 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' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
-        mkCase (EConstr.contract_case env sigma (ci, p', iv', c', bl'))
+      let bl' = Array.map2 f_ctx bl bl0 in
+      if pms==pms' && p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
+        mkCase (ci, u, pms', 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
@@ -760,8 +769,9 @@ let fold_constr_with_full_binders env sigma g f n acc c =
   | Proj (_,c) -> f n acc c
   | Evar (_,l) -> List.fold_left (f n) acc l
   | Case (ci, u, pms, p, iv, c, bl) ->
-    let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in
-    Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+    let (ci, _, pms, p, _, c, bl) = EConstr.annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+    let f_ctx acc (ctx, c) = f (List.fold_right g ctx n) acc c in
+    Array.fold_left f_ctx (f n (fold_invert (f n) (f_ctx (Array.fold_left (f n) acc pms) p) iv) c) bl
   | Fix (_,(lna,tl,bl)) ->
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in