+ 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 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,_)::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
+ branch::sort tl cltl
+ in
+ sort branches cl
+ | _ -> assert false