- let do_branch (pat, term) =
- match pat with
- | _ :: tl ->
- aux loc
- (List.fold_left (fun acc var -> (Cic.Name var) :: acc)
- context tl)
- term
- | [] -> assert false
+ let do_branch ((head, args), term) =
+ let (term_context, args_domain) =
+ List.fold_left
+ (fun (cont, dom) (name, typ) ->
+ (name :: cont,
+ (match typ with
+ | None -> dom
+ | Some typ -> Domain.union dom (aux loc cont typ))))
+ (context, Domain.empty) args
+ in
+ Domain.union (aux loc term_context term) args_domain