do_branch' context args
in
let (indtype_uri, indtype_no) =
- match resolve env (Id indty_ident) () with
- | Cic.MutInd (uri, tyno, _) -> uri, tyno
- | Cic.Implicit _ -> raise Try_again
- | _ -> raise DisambiguateChoices.Invalid_choice
+ match indty_ident with
+ | Some indty_ident ->
+ (match resolve env (Id indty_ident) () with
+ | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
+ | Cic.Implicit _ -> raise Try_again
+ | _ -> raise DisambiguateChoices.Invalid_choice)
+ | None ->
+ let fst_constructor =
+ match branches with
+ | ((head, _), _) :: _ -> head
+ | [] -> raise DisambiguateChoices.Invalid_choice
+ in
+ (match resolve env (Id fst_constructor) () with
+ | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
+ (indtype_uri, indtype_no)
+ | Cic.Implicit _ -> raise Try_again
+ | _ -> raise DisambiguateChoices.Invalid_choice)
in
Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
(List.map do_branch branches))
let branches_dom =
List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
in
- branches_dom @ outtype_dom @ term_dom @ [ Id indty_ident ]
+ branches_dom @ outtype_dom @ term_dom @
+ (match indty_ident with None -> [] | Some ident -> [ Id ident ])
| CicAst.LetIn ((var, typ), body, where) ->
let body_dom = aux loc context body in
let type_dom = aux_option loc context typ in