- if is_rewrite_right hd then
- let what, where = List.nth tl 5, List.nth tl 3 in
- let premise = mk_premise where in
- [P.Rewrite (true, what, Some (premise, name), dtext)]
- else if is_rewrite_left hd then
- let what, where = List.nth tl 5, List.nth tl 3 in
- let premise = mk_premise where in
- [P.Rewrite (false, what, Some (premise, name), dtext)]
- else begin match get_itype st v with
- | Some ty ->
- let qs = [[P.Id ""]; mk_proof (next st) v] in
- [P.Branch (qs, ""); P.Cut (name, ty, dtext)]
- | None ->
- let ty, _ = TC.type_of_aux' [] st.entries (cic hd) U.empty_ugraph in
- let (classes, rc) as h = L.classify ty in
- let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in
- [P.LetIn (name, v, dtext ^ text)]
+ if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else
+ if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
+ begin match get_inner_types st v with
+ | Some (ity, _) ->
+ let qs = [[T.Id ""]; mk_proof (next st) v] in
+ [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
+ | None ->
+ let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
+ let (classes, rc) as h = Cl.classify st.context ty in
+ let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
+ [T.LetIn (name, v, dtext ^ text)]