From a7ac10d52818a5f1b720474f015234933c3eab04 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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.5