let sname = match name with None -> "" | Some (id, _) -> id in
let note = Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s"
note sname (Pp.ppterm csty) (Pp.ppterm cety)
let sname = match name with None -> "" | Some (id, _) -> id in
let note = Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s"
note sname (Pp.ppterm csty) (Pp.ppterm cety)
| Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
let convert_elim st ?name t v pattern =
| Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
let convert_elim st ?name t v pattern =
and proc_appl st what hd tl =
let proceed, dtext = test_depth st in
let script = if proceed then
and proc_appl st what hd tl =
let proceed, dtext = test_depth st in
let script = if proceed then
- let ty = get_type "TC2" st hd in
+ let ty = match get_inner_types st hd with
+ | Some (ity, _) -> H.cic ity
+ | None -> get_type "TC2" st hd
+ in
let classes, rc = Cl.classify st.context ty in
let goal_arity, goal = match get_inner_types st what with
| None -> 0, None
let classes, rc = Cl.classify st.context ty in
let goal_arity, goal = match get_inner_types st what with
| None -> 0, None