off by one in calling count_from

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index f96a6f31782d3eb44f1743e9120bf02daff2fb83..19db6c5a3449f43764b9ceed5beea4d4a216d15a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1235,7 +1235,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
               function [] -> [] | v::tl -> (k,v)::enum_from (k+1) tl 
             in
             guarded_by_destructors 
-             ~subst ~metasenv context (enum_from (x+1) kl) m
+             ~subst ~metasenv context (enum_from (x+2) kl) m
           end else
            match returns_a_coinductive ~subst [] ty with
             | None ->