- if conclude.Con.conclude_method = "TD_Conversion" then
- make_concl "that is equivalent to" concl
- else make_concl "we conclude" concl in
- B.V ([], [conclude_body; ann_concl])
- | _ -> conclude_aux conclude in
- if indent then
- B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id],
- [tconclude_body]))
- else
- B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
+ if conclude.Con.conclude_method = "Intros+LetTac"
+ || conclude.Con.conclude_method = "ByInduction"
+ || conclude.Con.conclude_method = "TD_Conversion"
+ then
+ B.Text([],"")
+ else if omit_conclusion then B.Text([],"done.")
+ else B.b_hv []
+ ((if not is_top_down || omit_dot then [make_concl "we proved" concl; B.Text([],if not is_top_down then "(previous)" else "")] else [B.Text([],"done")]) @ if not omit_dot then [B.Text([],".")] else [])
+ in
+ B.V ([], [conclude_body; ann_concl])
+ | _ -> conclude_aux conclude
+ in
+ if indent then
+ B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id],
+ [tconclude_body]))
+ else
+ B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])