- let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in
+ let branches, branch_args = List.split branches_with_args in
+ let bo = NotationPt.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 (NotationPt.Implicit `JustOne)
+ (List.length args - 1) @
+ [mk_appl (mk_id name :: params @ cargs)]))))) branch_args @
+ List.map (function name -> name, None) args in