+ raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+ in
+ let branches =
+ match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
+ Cic.InductiveDefinition (il,_,_,_) ->
+ let _,_,_,cl =
+ try
+ 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
+ [] ->
+ if branches = [] then []
+ else
+ raise (Invalid_choice
+ (Some loc,
+ lazy
+ ("Unrecognized constructors: " ^
+ String.concat " "
+ (List.map (fun ((head,_,_),_) -> head) branches))))
+ | (name,ty)::cltl ->
+ let rec find_and_remove =
+ function
+ [] ->
+ raise
+ (Invalid_choice
+ (Some loc, lazy ("Missing case: " ^ name)))
+ | ((name',_,_),_) as branch :: tl when name = name' ->
+ branch,tl
+ | branch::tl ->
+ let found,rest = find_and_remove tl in
+ found, branch::rest
+ in
+ let branch,tl = find_and_remove branches in
+ 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