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

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 24c4faa348aa4e1c853b75ff5b5a79ae0b0cec5d..a99278dbcf137de171eff09cb3f5339fde9b8ab7 100644 (file)
--- 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