From a7ac10d52818a5f1b720474f015234933c3eab04 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Jul 2007 20:17:47 +0000 Subject: [PATCH] In place of conclude, obtain FIXMEXXX is now generated when required. --- helm/software/components/content_pres/content2pres.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 24c4faa34..a99278dbc 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -502,8 +502,14 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ ( | Con.Term (_,t) -> t | _ -> assert false in - B.HOV([],[B.b_kw "conclude";B.b_space;term2pres hd; (* B.b_space; *) - B.V ([],aux (List.tl conclude.Con.conclude_args))]) + if is_top_down then + B.HOV([], + [B.b_kw "conclude";B.b_space;term2pres hd; + B.V ([],aux (List.tl conclude.Con.conclude_args))]) + else + B.HOV([], + [B.b_kw "obtain";B.b_space;B.b_kw "FIXMEXX"; B.b_space;term2pres hd; + B.V ([],aux (List.tl conclude.Con.conclude_args))]) else if conclude.Con.conclude_method = "Apply" then let pres_args = make_args_for_apply term2pres conclude.Con.conclude_args in -- 2.39.2