From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Dec 2001 11:03:59 +0000 (+0000)
Subject: does_not_occur now handles LetIn correctly (i.e. raising an exception
X-Git-Tag: mlminidom_0_2_2~26
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5735143021bfe2b270f57e115d109a1f876faccc;p=helm.git

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 cea5a2772..1149bfa3b 100644
--- 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)