| CicNotationPt.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux loc context term in
let cic_outtype = aux_option loc context None outtype in
- let do_branch ((head, args), term) =
+ let do_branch ((head, _, args), term) =
let rec do_branch' context = function
| [] -> aux loc context term
| (name, typ) :: tl ->
in
let (indtype_uri, indtype_no) =
match indty_ident with
- | Some indty_ident ->
+ | Some (indty_ident, _) ->
(match resolve env (Id indty_ident) () with
| Cic.MutInd (uri, tyno, _) -> (uri, tyno)
| Cic.Implicit _ -> raise Try_again
| None ->
let fst_constructor =
match branches with
- | ((head, _), _) :: _ -> head
+ | ((head, _, _), _) :: _ -> head
| [] -> raise Invalid_choice
in
(match resolve env (Id fst_constructor) () with
let outtype_dom = domain_rev_of_term_option loc context outtype in
let get_first_constructor = function
| [] -> []
- | ((head, _), _) :: _ -> [ Id head ]
+ | ((head, _, _), _) :: _ -> [ Id head ]
in
- let do_branch ((head, args), term) =
+ let do_branch ((head, _, args), term) =
let (term_context, args_domain) =
List.fold_left
(fun (cont, dom) (name, typ) ->
branches_dom @ outtype_dom @ term_dom @
(match indty_ident with
| None -> get_first_constructor branches
- | Some ident -> [ Id ident ])
+ | Some (ident, _) -> [ Id ident ])
| CicNotationPt.Cast (term, ty) ->
let term_dom = domain_rev_of_term ~loc context term in
let ty_dom = domain_rev_of_term ~loc context ty in