- 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.H([], [B.b_kw "done" ; B.Text([],".") ])
+ else
+ B.b_hv []
+ ((if not is_top_down || omit_dot then
+ (make_concl "we proved" concl) ::
+ if not is_top_down then
+ [B.b_space; B.Text([],"(previous)")]
+ else []
+ else [B.b_kw "done"]
+ ) @ if not omit_dot then [B.Text([],".")] else [])
+ in
+ B.V ([], prequel @ [conclude_body; ann_concl])
+ | _ -> conclude_aux ?skip_initial_lambdas_internal 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])