From 5735143021bfe2b270f57e115d109a1f876faccc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Dec 2001 11:03:59 +0000 Subject: [PATCH] does_not_occur now handles LetIn correctly (i.e. raising an exception different from NotImplemented) --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) -- 2.39.2