- Ast.Box (kind, List.concat (List.map (subst env) tl))
- | l -> CicNotationUtil.visit_layout (subst_singleton env) l
+ let tl' = subst_children pos env tl in
+ Ast.Box (kind, List.concat tl')
+ | l -> CicNotationUtil.visit_layout (subst_singleton pos env) l
+ and subst_children pos env =
+ function
+ | [] -> []
+ | [ child ] ->
+ let pos' =
+ match pos with
+ | `Inner -> `Right
+ | `Left -> `Left
+ | `None -> assert false
+ | `Right -> `Right
+ in
+ [ subst pos' env child ]
+ | hd :: tl ->
+ let pos' =
+ match pos with
+ | `Inner -> `Inner
+ | `Left -> `Inner
+ | `None -> assert false
+ | `Right -> `Right
+ in
+ (subst pos env hd) :: subst_children pos' env tl