]> matita.cs.unibo.it Git - helm.git/commitdiff
Ooops. In previous commit I forgot to subtract the left arguments in case
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 25 Oct 2007 16:57:04 +0000 (16:57 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 25 Oct 2007 16:57:04 +0000 (16:57 +0000)
analysis.

helm/software/components/cic_disambiguation/disambiguate.ml

index 6dd82cc288c42731702bd8b94220d31b5502e8a9..3d671cd7fd62b5b4fa800559dd80fb79b34a2939 100644 (file)
@@ -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