- let _, row, ds = List.fold_left (mk_arg false) step0 (List.tl cargs) in
- Cic.AAppl (aref, List.rev row), ds
-
-and mk_delta p ds =
- let cmethod = p.C.proof_conclude.C.conclude_method in
- let cargs = p.C.proof_conclude.C.conclude_args in
- let capply = p.C.proof_apply_context in
- let ccont = p.C.proof_context in
- let caref = p.C.proof_conclude.C.conclude_aref in
- match cmethod with
- | "Exact"
- | "Apply" when ccont = [] ->
- let what, ds = mk_apply_term caref capply ds cargs in
- let name = "PREVIOUS" in
- mk_arel 1 name, LetIn (name, what, "") :: ds
- | _ -> mk_arel 1 "COMPOUND", ds
+ let ac, row, ds = List.fold_left (mk_arg false) step0 (List.tl cargs) in
+ ac, ds, Cic.AAppl (aref, List.rev row)
+
+and mk_delta ac ds = match ac with
+ | p :: ac ->
+ let cmethod = p.C.proof_conclude.C.conclude_method in
+ let cargs = p.C.proof_conclude.C.conclude_args in
+ let capply = p.C.proof_apply_context in
+ let ccont = p.C.proof_context in
+ let caref = p.C.proof_conclude.C.conclude_aref in
+ begin match cmethod with
+ | "Exact"
+ | "Apply" when ccont = [] && capply = [] ->
+ let ac, ds, what = mk_apply_term caref ac ds cargs in
+ let name = "PREVIOUS" in
+ ac, mk_arel 1 name, LetIn (name, what, "") :: ds
+ | _ -> ac, mk_arel 1 "COMPOUND", ds
+ end
+ | _ -> assert false