does_not_occur now handles LetIn correctly (i.e. raising an exception

different from NotImplemented)

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index cea5a277218213cbc09da878b4256899e2f5ae8b..1149bfa3b7dd661a91e6f839c2f72d6911576377 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -433,8 +433,8 @@ and recursive_args n nn te =
    | 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)