From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Jul 2007 20:17:47 +0000 (+0000)
Subject: In place of conclude, obtain FIXMEXXX is now generated when required.
X-Git-Tag: 0.4.95@7852~370
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1dbbb98181ab7c40ed2da6a941a69833b00a6aae;p=helm.git

In place of conclude, obtain FIXMEXXX is now generated when required.
---

diff --git a/components/content_pres/content2pres.ml b/components/content_pres/content2pres.ml
index 24c4faa34..a99278dbc 100644
--- a/components/content_pres/content2pres.ml
+++ b/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