- let branches, branch_args = List.split branches_with_args in
- let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),Some p_name,branches) in
- let final_params =
- List.map (function name -> name, None) params @
- [p_name,Some p_ty] @
- List.map (function name, cargs, nih ->
- name_of_k name,
- Some (mk_prods cargs (mk_arrs nih
- (mk_appl
- (p_name::HExtlib.mk_list (CicNotationPt.Implicit `JustOne)
- (List.length args - 1) @
- [mk_appl (mk_id name :: params @ cargs)]))))) branch_args @
- List.map (function name -> name, None) args in
+ let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in