From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 3 Apr 2008 16:23:04 +0000 (+0000)
Subject: non debruijned constructor may be useless elswere, for the moment we do not bind it
X-Git-Tag: make_still_working~5463
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a287d1b295b81866d6aba85955cc835a57e9ae9e;p=helm.git

non debruijned constructor may be useless elswere, for the moment we do not bind it
---

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)