From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 1 Aug 2008 07:34:13 +0000 (+0000)
Subject: fixed recursiveness check
X-Git-Tag: make_still_working~4867
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f5ee9e3667439a473bac6b80f4b5865ee1c6b14a;p=helm.git

fixed recursiveness check
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c68982ff7..cf445a8f0 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -689,7 +689,16 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
 and is_non_recursive_singleton (Ref.Ref (uri,_)) iname ity cty =
      let ctx = [iname, C.Decl ity] in
      let cty = debruijn uri 1 [] cty in
-     does_not_occur ~subst:[] ctx 0 1 cty
+     let len = List.length ctx in
+     let rec aux ctx n nn t =
+       match R.whd ctx t with
+       | C.Prod (name, src, tgt) ->
+            does_not_occur ~subst:[] ctx n nn src &&
+             aux ((name, C.Decl src) :: ctx) (n+1) (nn+1) tgt
+       | C.Rel k | C.Appl (C.Rel k :: _) when k = nn -> true
+       | _ -> assert false
+     in
+     aux ctx (len-1) len cty
 
 and is_non_informative paramsno c =
  let rec aux context c =