- 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)