different from NotImplemented)
| C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
| C.Prod (_,so,de) ->
(not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
| C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
| C.Prod (_,so,de) ->
(not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
- | C.Lambda _ -> raise (Impossible 4) (* due to type-checking *)
- | C.LetIn _ -> raise NotImplemented
+ | C.Lambda _
+ | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *)
| C.Appl _ -> []
| C.Const _
| C.Abst _ -> raise (Impossible 5)
| C.Appl _ -> []
| C.Const _
| C.Abst _ -> raise (Impossible 5)