Bug fixed: case analysis where a case had not the expected number of arguments

was not detected.

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 020d038ac74ff687dec0a0fd30062a9c358eef85..6dd82cc288c42731702bd8b94220d31b5502e8a9 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -253,6 +253,11 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                List.nth il indtype_no
               with _ -> assert false
              in
+              let rec count_prod t =
+                match CicReduction.whd [] t with
+                    Cic.Prod (_, _, t) -> 1 + (count_prod t)
+                  | _ -> 0 
+              in 
               let rec sort branches cl =
                match cl with
                   [] ->
@@ -264,7 +269,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                        ("Unrecognized constructors: " ^
                         String.concat " "
                          (List.map (fun ((head,_,_),_) -> head) branches))))
-                | (name,_)::cltl ->
+                | (name,ty)::cltl ->
                    let rec find_and_remove =
                     function
                        [] ->
@@ -278,7 +283,14 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                          found, branch::rest
                    in
                     let branch,tl = find_and_remove branches in
-                     branch::sort tl cltl
+                    let (_,_,args),_ = branch in
+                     if List.length args = count_prod ty then
+                      branch::sort tl cltl
+                     else
+                      raise
+                       (Invalid_choice
+                        (Some loc,
+                          lazy ("Wrong number of arguments for " ^ name)))
               in
                sort branches cl
           | _ -> assert false