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 4679de20a047f9f7685a8059cf57e05727f69c62..80d4dea0ec3bae7c8648a6d5043a4a6f39faa6a8 100644 (file)
--- 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)