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