From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 25 Oct 2007 16:57:04 +0000 (+0000)
Subject: Ooops. In previous commit I forgot to subtract the left arguments in case
X-Git-Tag: make_still_working~5948
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b6f67d53a7772e7872356412fd470ca5b92e2bdb;p=helm.git

Ooops. In previous commit I forgot to subtract the left arguments in case
analysis.
---

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 6dd82cc28..3d671cd7f 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -247,7 +247,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
         in
         let branches =
          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
-            Cic.InductiveDefinition (il,_,_,_) ->
+            Cic.InductiveDefinition (il,_,leftsno,_) ->
              let _,_,_,cl =
               try
                List.nth il indtype_no
@@ -284,7 +284,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                    in
                     let branch,tl = find_and_remove branches in
                     let (_,_,args),_ = branch in
-                     if List.length args = count_prod ty then
+                     if List.length args = count_prod ty - leftsno then
                       branch::sort tl cltl
                      else
                       raise