+ | NCic.Lambda (n,s,t) ->
+ (* Lambdas can me met in branches of matches, expecially when the
+ output type is a product *)
+ classify_not_term status ((n,NCic.Decl s)::context) t
+ | NCic.Match (r,_,_,pl) ->
+ let classified_pl = List.map (classify_not_term status context) pl in
+ sup classified_pl