From a287d1b295b81866d6aba85955cc835a57e9ae9e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 3 Apr 2008 16:23:04 +0000 Subject: [PATCH] non debruijned constructor may be useless elswere, for the moment we do not bind it --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 4679de20a..80d4dea0e 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -1083,7 +1083,7 @@ and guarded_by_destructors ~subst context recfuns t = aux k outtype; List.iter (aux k) args; List.iter2 - (fun p (_,c,bruijnedc) -> + (fun p (_,_,bruijnedc) -> let rl = recursive_args ~subst lefts_and_tys 0 len bruijnedc in let p, k = get_new_safes ~subst k p rl in aux k p) -- 2.39.2