let parsno, argsno = List.length classes, List.length tl in
let decurry = parsno - argsno in
let diff = goal_arity - decurry in
- if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (H.cic hd)));
+ if diff < 0 then
+ let text = Printf.sprintf "partial application: %i" diff in
+ [T.Exact (what, dtext ^ text)]
+ else
let classes = Cl.adjust st.context tl ?goal classes in
let rec mk_synth a n =
if n < 0 then a else mk_synth (I.S.add n a) (pred n)
let script = List.rev (mk_arg st hd) in
let tactic b t n = if b then T.Apply (t, n) else T.Exact (t, n) in
match rc with
- | Some (i, j, uri, tyno) ->
+ | Some (i, j, uri, tyno) when decurry = 0 ->
let classes2, tl2, _, where = split2_last classes tl in
let script2 = List.rev (mk_arg st where) @ script in
let synth2 = I.S.add 1 synth in
let using = Some hd in
script2 @
[T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
- | None ->
+ | _ ->
let names = get_sub_names hd tl in
let qs = proc_bkd_proofs (next st) synth names classes tl in
let b, hd = mk_exp_args hd tl classes synth in