From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 7 Apr 2008 10:54:41 +0000 (+0000)
Subject: off by one in calling count_from
X-Git-Tag: make_still_working~5436
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8ec032a2241f346e9443b8ddcc0b4f81965893d9;p=helm.git

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 f96a6f317..19db6c5a3 100644
--- 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 ->