- | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
- | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
- | _ -> assert false in aux ty in
- status, o_t, NotationPt.NCic ty, source, target in
+ | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
+ | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
+ | _ -> assert false
+ in
+ aux ty
+ in
+ status, o_t, NotationPt.NCic ty, source, target
+ in