X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=477697580fd4df83314ad345634a798b47870237;hb=f8cc3ca9341553197c08cc217f787b663787d758;hp=a99278dbcf137de171eff09cb3f5339fde9b8ab7;hpb=a7ac10d52818a5f1b720474f015234933c3eab04;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index a99278dbc..477697580 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -181,7 +181,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
            | _ -> p.Con.proof_context)
           presacontext
     in
+(*
 let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (if is_top_down then "(TD)" else "(NTD)") ^ "*)"); body; B.b_kw "(*>>*)"]) in
+*)
     match p.Con.proof_name with
       None -> body
     | Some name ->
@@ -447,9 +449,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
         | Some j -> [j]
       in
       let index_term1, index_term2 =
-       if  (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
-        || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down)
-       then 2,5 else 5,2
+       if conclude.Con.conclude_method = "RewriteLR" then 2,5 else 5,2
       in
       let term1 = 
         (match List.nth conclude.Con.conclude_args index_term1 with