]> matita.cs.unibo.it Git - helm.git/commitdiff
In place of conclude, obtain FIXMEXXX is now generated when required.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 4 Jul 2007 20:17:47 +0000 (20:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 4 Jul 2007 20:17:47 +0000 (20:17 +0000)
components/content_pres/content2pres.ml

index 24c4faa348aa4e1c853b75ff5b5a79ae0b0cec5d..a99278dbcf137de171eff09cb3f5339fde9b8ab7 100644 (file)
@@ -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