fixed recursiveness check

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c68982ff7dddea804aba27eeb53b8f478d62cfdf..cf445a8f0fc28d0d562238ecc053fd719186527c 100644 (file)
--- 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 =